Theorem axextnd

Description: A version of the Axiom of Extensionality with no distinct variable conditions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 14-Aug-2003) (New usage is discouraged.)

	Ref	Expression
Assertion	axextnd	$$⊢\exists x\left(\left(x\in y\leftrightarrow x\in z\right)\to y=z\right)$$

Proof

Step	Hyp	Ref	Expression
1		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
2		nfnae	$$⊢Ⅎx\neg \forall xx=z$$
3	1 2	nfan	$$⊢Ⅎx\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)$$
4		nfcvf	$$⊢\neg \forall xx=y\to \underset{\_}{Ⅎ}xy$$
5	4	adantr	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}xy$$
6	5	nfcrd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎxw\in y$$
7		nfcvf	$$⊢\neg \forall xx=z\to \underset{\_}{Ⅎ}xz$$
8	7	adantl	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \underset{\_}{Ⅎ}xz$$
9	8	nfcrd	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎxw\in z$$
10	6 9	nfbid	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to Ⅎx\left(w\in y\leftrightarrow w\in z\right)$$
11		elequ1	$$⊢w=x\to \left(w\in y\leftrightarrow x\in y\right)$$
12		elequ1	$$⊢w=x\to \left(w\in z\leftrightarrow x\in z\right)$$
13	11 12	bibi12d	$$⊢w=x\to \left(\left(w\in y\leftrightarrow w\in z\right)\leftrightarrow \left(x\in y\leftrightarrow x\in z\right)\right)$$
14	13	a1i	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(w=x\to \left(\left(w\in y\leftrightarrow w\in z\right)\leftrightarrow \left(x\in y\leftrightarrow x\in z\right)\right)\right)$$
15	3 10 14	cbvald	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(\forall w\left(w\in y\leftrightarrow w\in z\right)\leftrightarrow \forall x\left(x\in y\leftrightarrow x\in z\right)\right)$$
16		axextg	$$⊢\forall w\left(w\in y\leftrightarrow w\in z\right)\to y=z$$
17	15 16	syl6bir	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(\forall x\left(x\in y\leftrightarrow x\in z\right)\to y=z\right)$$
18		19.8a	$$⊢y=z\to \exists xy=z$$
19	17 18	syl6	$$⊢\left(\neg \forall xx=y\wedge \neg \forall xx=z\right)\to \left(\forall x\left(x\in y\leftrightarrow x\in z\right)\to \exists xy=z\right)$$
20	19	ex	$$⊢\neg \forall xx=y\to \left(\neg \forall xx=z\to \left(\forall x\left(x\in y\leftrightarrow x\in z\right)\to \exists xy=z\right)\right)$$
21		ax6e	$$⊢\exists xx=z$$
22		ax7	$$⊢x=y\to \left(x=z\to y=z\right)$$
23	22	aleximi	$$⊢\forall xx=y\to \left(\exists xx=z\to \exists xy=z\right)$$
24	21 23	mpi	$$⊢\forall xx=y\to \exists xy=z$$
25	24	a1d	$$⊢\forall xx=y\to \left(\forall x\left(x\in y\leftrightarrow x\in z\right)\to \exists xy=z\right)$$
26		ax6e	$$⊢\exists xx=y$$
27		ax7	$$⊢x=z\to \left(x=y\to z=y\right)$$
28		equcomi	$$⊢z=y\to y=z$$
29	27 28	syl6	$$⊢x=z\to \left(x=y\to y=z\right)$$
30	29	aleximi	$$⊢\forall xx=z\to \left(\exists xx=y\to \exists xy=z\right)$$
31	26 30	mpi	$$⊢\forall xx=z\to \exists xy=z$$
32	31	a1d	$$⊢\forall xx=z\to \left(\forall x\left(x\in y\leftrightarrow x\in z\right)\to \exists xy=z\right)$$
33	20 25 32	pm2.61ii	$$⊢\forall x\left(x\in y\leftrightarrow x\in z\right)\to \exists xy=z$$
34	33	19.35ri	$$⊢\exists x\left(\left(x\in y\leftrightarrow x\in z\right)\to y=z\right)$$