Theorem axextdist

Description: ax-ext with distinctors instead of distinct variable conditions. (Contributed by Scott Fenton, 13-Dec-2010)

	Ref	Expression
Assertion	axextdist	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(\forall z\left(z\in x\leftrightarrow z\in y\right)\to x=y\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfnae	$$⊢Ⅎz\neg \forall zz=x$$
2		nfnae	$$⊢Ⅎz\neg \forall zz=y$$
3	1 2	nfan	$$⊢Ⅎz\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)$$
4		nfcvf	$$⊢\neg \forall zz=x\to \underset{\_}{Ⅎ}zx$$
5	4	adantr	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \underset{\_}{Ⅎ}zx$$
6	5	nfcrd	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to Ⅎzw\in x$$
7		nfcvf	$$⊢\neg \forall zz=y\to \underset{\_}{Ⅎ}zy$$
8	7	adantl	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \underset{\_}{Ⅎ}zy$$
9	8	nfcrd	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to Ⅎzw\in y$$
10	6 9	nfbid	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to Ⅎz\left(w\in x\leftrightarrow w\in y\right)$$
11		elequ1	$$⊢w=z\to \left(w\in x\leftrightarrow z\in x\right)$$
12		elequ1	$$⊢w=z\to \left(w\in y\leftrightarrow z\in y\right)$$
13	11 12	bibi12d	$$⊢w=z\to \left(\left(w\in x\leftrightarrow w\in y\right)\leftrightarrow \left(z\in x\leftrightarrow z\in y\right)\right)$$
14	13	a1i	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(w=z\to \left(\left(w\in x\leftrightarrow w\in y\right)\leftrightarrow \left(z\in x\leftrightarrow z\in y\right)\right)\right)$$
15	3 10 14	cbvald	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(\forall w\left(w\in x\leftrightarrow w\in y\right)\leftrightarrow \forall z\left(z\in x\leftrightarrow z\in y\right)\right)$$
16		axextg	$$⊢\forall w\left(w\in x\leftrightarrow w\in y\right)\to x=y$$
17	15 16	syl6bir	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(\forall z\left(z\in x\leftrightarrow z\in y\right)\to x=y\right)$$