Theorem ax6vsep

Description: Derive ax6v (a weakened version of ax-6 where x and y must be distinct), from Separation ax-sep and Extensionality ax-ext . See ax6 for the derivation of ax-6 from ax6v . (Contributed by NM, 12-Nov-2013) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ax6vsep	$$⊢\neg \forall x\neg x=y$$

Proof

Step	Hyp	Ref	Expression
1		ax-sep	$$⊢\exists x\forall z\left(z\in x\leftrightarrow \left(z\in y\wedge \left(z=z\to z=z\right)\right)\right)$$
2		id	$$⊢z=z\to z=z$$
3	2	biantru	$$⊢z\in y\leftrightarrow \left(z\in y\wedge \left(z=z\to z=z\right)\right)$$
4	3	bibi2i	$$⊢\left(z\in x\leftrightarrow z\in y\right)\leftrightarrow \left(z\in x\leftrightarrow \left(z\in y\wedge \left(z=z\to z=z\right)\right)\right)$$
5	4	biimpri	$$⊢\left(z\in x\leftrightarrow \left(z\in y\wedge \left(z=z\to z=z\right)\right)\right)\to \left(z\in x\leftrightarrow z\in y\right)$$
6	5	alimi	$$⊢\forall z\left(z\in x\leftrightarrow \left(z\in y\wedge \left(z=z\to z=z\right)\right)\right)\to \forall z\left(z\in x\leftrightarrow z\in y\right)$$
7		ax-ext	$$⊢\forall z\left(z\in x\leftrightarrow z\in y\right)\to x=y$$
8	6 7	syl	$$⊢\forall z\left(z\in x\leftrightarrow \left(z\in y\wedge \left(z=z\to z=z\right)\right)\right)\to x=y$$
9	8	eximi	$$⊢\exists x\forall z\left(z\in x\leftrightarrow \left(z\in y\wedge \left(z=z\to z=z\right)\right)\right)\to \exists xx=y$$
10	1 9	ax-mp	$$⊢\exists xx=y$$
11		df-ex	$$⊢\exists xx=y\leftrightarrow \neg \forall x\neg x=y$$
12	10 11	mpbi	$$⊢\neg \forall x\neg x=y$$