Theorem axc14

Description: 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.)

	Ref	Expression
Assertion	axc14	$$⊢\neg \forall zz=x\to \left(\neg \forall zz=y\to \left(x\in y\to \forall zx\in y\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		hbn1	$$⊢\neg \forall zz=y\to \forall z\neg \forall zz=y$$
2		dveel2	$$⊢\neg \forall zz=y\to \left(w\in y\to \forall zw\in y\right)$$
3	1 2	hbim1	$$⊢\left(\neg \forall zz=y\to w\in y\right)\to \forall z\left(\neg \forall zz=y\to w\in y\right)$$
4		elequ1	$$⊢w=x\to \left(w\in y\leftrightarrow x\in y\right)$$
5	4	imbi2d	$$⊢w=x\to \left(\left(\neg \forall zz=y\to w\in y\right)\leftrightarrow \left(\neg \forall zz=y\to x\in y\right)\right)$$
6	3 5	dvelim	$$⊢\neg \forall zz=x\to \left(\left(\neg \forall zz=y\to x\in y\right)\to \forall z\left(\neg \forall zz=y\to x\in y\right)\right)$$
7		nfa1	$$⊢Ⅎz\forall zz=y$$
8	7	nfn	$$⊢Ⅎz\neg \forall zz=y$$
9	8	19.21	$$⊢\forall z\left(\neg \forall zz=y\to x\in y\right)\leftrightarrow \left(\neg \forall zz=y\to \forall zx\in y\right)$$
10	6 9	syl6ib	$$⊢\neg \forall zz=x\to \left(\left(\neg \forall zz=y\to x\in y\right)\to \left(\neg \forall zz=y\to \forall zx\in y\right)\right)$$
11	10	pm2.86d	$$⊢\neg \forall zz=x\to \left(\neg \forall zz=y\to \left(x\in y\to \forall zx\in y\right)\right)$$