Theorem axextbdist

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

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

Proof

Step	Hyp	Ref	Expression
1		axc9	$$⊢\neg \forall zz=x\to \left(\neg \forall zz=y\to \left(x=y\to \forall zx=y\right)\right)$$
2	1	imp	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(x=y\to \forall zx=y\right)$$
3		nfnae	$$⊢Ⅎz\neg \forall zz=x$$
4		nfnae	$$⊢Ⅎz\neg \forall zz=y$$
5	3 4	nfan	$$⊢Ⅎz\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)$$
6		elequ2	$$⊢x=y\to \left(z\in x\leftrightarrow z\in y\right)$$
7	6	a1i	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(x=y\to \left(z\in x\leftrightarrow z\in y\right)\right)$$
8	5 7	alimd	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(\forall zx=y\to \forall z\left(z\in x\leftrightarrow z\in y\right)\right)$$
9	2 8	syld	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(x=y\to \forall z\left(z\in x\leftrightarrow z\in y\right)\right)$$
10		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)$$
11	9 10	impbid	$$⊢\left(\neg \forall zz=x\wedge \neg \forall zz=y\right)\to \left(x=y\leftrightarrow \forall z\left(z\in x\leftrightarrow z\in y\right)\right)$$