Theorem ax6e2ndVD

Description: The following User's Proof is a Virtual Deduction proof (see wvd1 ) completed automatically by a Metamath tools program invoking mmj2 and the Metamath Proof Assistant. ax6e2nd is ax6e2ndVD without virtual deductions and was automatically derived from ax6e2ndVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Assertion	ax6e2ndVD	$$⊢\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	e0a	$$⊢\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		idn1	$$⊢\left(\neg \forall xx=y\to \neg \forall xx=y\right)$$
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		idn1	$$⊢\left(z=y\to z=y\right)$$
17		equequ1	$$⊢z=y\to \left(z=v\leftrightarrow y=v\right)$$
18	16 17	e1a	$$⊢\left(z=y\to \left(z=v\leftrightarrow y=v\right)\right)$$
19	18	in1	$$⊢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	e1a	$$⊢\left(\neg \forall xx=y\to \left(y=v\to \forall xy=v\right)\right)$$
22	21	in1	$$⊢\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	e1a	$$⊢\left(\neg \forall xx=y\to \forall x\left(y=v\to \forall xy=v\right)\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	e1a	$$⊢\left(\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)\right)$$
28	27	in1	$$⊢\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	e1a	$$⊢\left(\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)\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	e1a	$$⊢\left(\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)\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	e01	$$⊢\left(\neg \forall xx=y\to \exists y\exists x\left(x=u\wedge y=v\right)\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	e1a	$$⊢\left(\neg \forall xx=y\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$
38	37	in1	$$⊢\neg \forall xx=y\to \exists x\exists y\left(x=u\wedge y=v\right)$$