Theorem axc14
Axiom [ax-c14] is redundant if we assume [ax-5]. Remark 9.6 in
[Megill] p. 448 (p. 16 of the preprint), regarding axiom scheme C14'.
Note that \( w \) is a dummy variable introduced in the proof. Its
purpose is to satisfy the distinct variable requirements of dveel2 and
[ax-5]. By the end of the proof it has vanished, and the final theorem
has no distinct variable requirements. Usage of this theorem is
discouraged because it depends on [ax-13]. (Contributed by NM,
29-Jun-1995.) (Proof modification is discouraged.)
(New usage is discouraged.)
Conclusion
\( \vdash \neg \forall z \, z = x \rightarrow \neg \forall z \, z = y \rightarrow x \in y \rightarrow \forall z \, x \in y \)
Proof
l0
hbn1
dveel2
l2
hbim1 l0 _
\( \vdash (\neg \forall z \, z = y \rightarrow w \in y) \rightarrow \forall z \, (\neg \forall z \, z = y \rightarrow w \in y) \)
elequ1
imbi2d _
\( \vdash w = x \rightarrow (\neg \forall z \, z = y \rightarrow w \in y \leftrightarrow \neg \forall z \, z = y \rightarrow x \in y) \)
l5
dvelim l2 _
\( \vdash \neg \forall z \, z = x \rightarrow (\neg \forall z \, z = y \rightarrow x \in y) \rightarrow \forall z \, (\neg \forall z \, z = y \rightarrow x \in y) \)
nfa1
nfn _
19.21 _
\( \vdash \forall z \, (\neg \forall z \, z = y \rightarrow x \in y) \leftrightarrow \neg \forall z \, z = y \rightarrow \forall z \, x \in y \)
imbitrdi l5 _
pm2.86d _