Theorem ax6e2nd

Description: If at least two sets exist ( dtru ), then the same is true expressed in an alternate form similar to the form of ax6e . ax6e2nd is derived from ax6e2ndVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ax6e2nd	$$⊢\neg \forall xx=y\to \exists x\exists y\left(x=u\wedge y=v\right)$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢u\in \mathrm{V}$$
2		ax6e	$$⊢\exists yy=v$$
3	1 2	pm3.2i	$$⊢\left(u\in \mathrm{V}\wedge \exists yy=v\right)$$
4		19.42v	$$⊢\exists y\left(u\in \mathrm{V}\wedge y=v\right)\leftrightarrow \left(u\in \mathrm{V}\wedge \exists yy=v\right)$$
5	4	biimpri	$$⊢\left(u\in \mathrm{V}\wedge \exists yy=v\right)\to \exists y\left(u\in \mathrm{V}\wedge y=v\right)$$
6	3 5	ax-mp	$$⊢\exists y\left(u\in \mathrm{V}\wedge y=v\right)$$
7		isset	$$⊢u\in \mathrm{V}\leftrightarrow \exists xx=u$$
8	7	anbi1i	$$⊢\left(u\in \mathrm{V}\wedge y=v\right)\leftrightarrow \left(\exists xx=u\wedge y=v\right)$$
9	8	exbii	$$⊢\exists y\left(u\in \mathrm{V}\wedge y=v\right)\leftrightarrow \exists y\left(\exists xx=u\wedge y=v\right)$$
10	6 9	mpbi	$$⊢\exists y\left(\exists xx=u\wedge y=v\right)$$
11		id	$$⊢\neg \forall xx=y\to \neg \forall xx=y$$
12		hbnae	$$⊢\neg \forall xx=y\to \forall y\neg \forall xx=y$$
13		hbn1	$$⊢\neg \forall xx=y\to \forall x\neg \forall xx=y$$
14		ax-5	$$⊢z=v\to \forall xz=v$$
15		ax-5	$$⊢y=v\to \forall zy=v$$
16		id	$$⊢z=y\to z=y$$
17		equequ1	$$⊢z=y\to \left(z=v\leftrightarrow y=v\right)$$
18	16 17	syl	$$⊢z=y\to \left(z=v\leftrightarrow y=v\right)$$
19	18	idiALT	$$⊢z=y\to \left(z=v\leftrightarrow y=v\right)$$
20	14 15 19	dvelimh	$$⊢\neg \forall xx=y\to \left(y=v\to \forall xy=v\right)$$
21	11 20	syl	$$⊢\neg \forall xx=y\to \left(y=v\to \forall xy=v\right)$$
22	21	idiALT	$$⊢\neg \forall xx=y\to \left(y=v\to \forall xy=v\right)$$
23	22	alimi	$$⊢\forall x\neg \forall xx=y\to \forall x\left(y=v\to \forall xy=v\right)$$
24	13 23	syl	$$⊢\neg \forall xx=y\to \forall x\left(y=v\to \forall xy=v\right)$$
25	11 24	syl	$$⊢\neg \forall xx=y\to \forall x\left(y=v\to \forall xy=v\right)$$
26		19.41rg	$$⊢\forall x\left(y=v\to \forall xy=v\right)\to \left(\left(\exists xx=u\wedge y=v\right)\to \exists x\left(x=u\wedge y=v\right)\right)$$
27	25 26	syl	$$⊢\neg \forall xx=y\to \left(\left(\exists xx=u\wedge y=v\right)\to \exists x\left(x=u\wedge y=v\right)\right)$$
28	27	idiALT	$$⊢\neg \forall xx=y\to \left(\left(\exists xx=u\wedge y=v\right)\to \exists x\left(x=u\wedge y=v\right)\right)$$
29	28	alimi	$$⊢\forall y\neg \forall xx=y\to \forall y\left(\left(\exists xx=u\wedge y=v\right)\to \exists x\left(x=u\wedge y=v\right)\right)$$
30	12 29	syl	$$⊢\neg \forall xx=y\to \forall y\left(\left(\exists xx=u\wedge y=v\right)\to \exists x\left(x=u\wedge y=v\right)\right)$$
31	11 30	syl	$$⊢\neg \forall xx=y\to \forall y\left(\left(\exists xx=u\wedge y=v\right)\to \exists x\left(x=u\wedge y=v\right)\right)$$
32		exim	$$⊢\forall y\left(\left(\exists xx=u\wedge y=v\right)\to \exists x\left(x=u\wedge y=v\right)\right)\to \left(\exists y\left(\exists xx=u\wedge y=v\right)\to \exists y\exists x\left(x=u\wedge y=v\right)\right)$$
33	31 32	syl	$$⊢\neg \forall xx=y\to \left(\exists y\left(\exists xx=u\wedge y=v\right)\to \exists y\exists x\left(x=u\wedge y=v\right)\right)$$
34		pm2.27	$$⊢\exists y\left(\exists xx=u\wedge y=v\right)\to \left(\left(\exists y\left(\exists xx=u\wedge y=v\right)\to \exists y\exists x\left(x=u\wedge y=v\right)\right)\to \exists y\exists x\left(x=u\wedge y=v\right)\right)$$
35	10 33 34	mpsyl	$$⊢\neg \forall xx=y\to \exists y\exists x\left(x=u\wedge y=v\right)$$
36		excomim	$$⊢\exists y\exists x\left(x=u\wedge y=v\right)\to \exists x\exists y\left(x=u\wedge y=v\right)$$
37	35 36	syl	$$⊢\neg \forall xx=y\to \exists x\exists y\left(x=u\wedge y=v\right)$$
38	37	idiALT	$$⊢\neg \forall xx=y\to \exists x\exists y\left(x=u\wedge y=v\right)$$