Theorem ax6e2ndeqVD

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. ax6e2eq is ax6e2ndeqVD without virtual deductions and was automatically derived from ax6e2ndeqVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax6e2nd	$$⊢\neg \forall xx=y\to \exists x\exists y\left(x=u\wedge y=v\right)$$
2		ax6e2eq	$$⊢\forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$
3	1	a1d	$$⊢\neg \forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)$$
4		exmid	$$⊢\left(\forall xx=y\vee \neg \forall xx=y\right)$$
5		jao	$$⊢\left(\forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)\to \left(\left(\neg \forall xx=y\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)\to \left(\left(\forall xx=y\vee \neg \forall xx=y\right)\to \left(u=v\to \exists x\exists y\left(x=u\wedge y=v\right)\right)\right)\right)$$
6	2 3 4 5	e000	$$⊢u=v\to \exists x\exists y\left(x=u\wedge y=v\right)$$
7	1 6	jaoi	$$⊢\left(\neg \forall xx=y\vee u=v\right)\to \exists x\exists y\left(x=u\wedge y=v\right)$$
8		idn1	$$⊢\left(u\ne v\to u\ne v\right)$$
9		idn2	$$⊢\left(u\ne v,\left(x=u\wedge y=v\right)\to \left(x=u\wedge y=v\right)\right)$$
10		simpl	$$⊢\left(x=u\wedge y=v\right)\to x=u$$
11	9 10	e2	$$⊢\left(u\ne v,\left(x=u\wedge y=v\right)\to x=u\right)$$
12		neeq1	$$⊢x=u\to \left(x\ne v\leftrightarrow u\ne v\right)$$
13	12	biimprcd	$$⊢u\ne v\to \left(x=u\to x\ne v\right)$$
14	8 11 13	e12	$$⊢\left(u\ne v,\left(x=u\wedge y=v\right)\to x\ne v\right)$$
15		simpr	$$⊢\left(x=u\wedge y=v\right)\to y=v$$
16	9 15	e2	$$⊢\left(u\ne v,\left(x=u\wedge y=v\right)\to y=v\right)$$
17		neeq2	$$⊢y=v\to \left(x\ne y\leftrightarrow x\ne v\right)$$
18	17	biimprcd	$$⊢x\ne v\to \left(y=v\to x\ne y\right)$$
19	14 16 18	e22	$$⊢\left(u\ne v,\left(x=u\wedge y=v\right)\to x\ne y\right)$$
20		df-ne	$$⊢x\ne y\leftrightarrow \neg x=y$$
21	20	bicomi	$$⊢\neg x=y\leftrightarrow x\ne y$$
22		sp	$$⊢\forall xx=y\to x=y$$
23	22	con3i	$$⊢\neg x=y\to \neg \forall xx=y$$
24	21 23	sylbir	$$⊢x\ne y\to \neg \forall xx=y$$
25	19 24	e2	$$⊢\left(u\ne v,\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)$$
26	25	in2	$$⊢\left(u\ne v\to \left(\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\right)$$
27	26	gen11	$$⊢\left(u\ne v\to \forall x\left(\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\right)$$
28		exim	$$⊢\forall x\left(\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\to \left(\exists x\left(x=u\wedge y=v\right)\to \exists x\neg \forall xx=y\right)$$
29	27 28	e1a	$$⊢\left(u\ne v\to \left(\exists x\left(x=u\wedge y=v\right)\to \exists x\neg \forall xx=y\right)\right)$$
30		nfnae	$$⊢Ⅎx\neg \forall xx=y$$
31	30	19.9	$$⊢\exists x\neg \forall xx=y\leftrightarrow \neg \forall xx=y$$
32		imbi2	$$⊢\left(\exists x\neg \forall xx=y\leftrightarrow \neg \forall xx=y\right)\to \left(\left(\exists x\left(x=u\wedge y=v\right)\to \exists x\neg \forall xx=y\right)\leftrightarrow \left(\exists x\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\right)$$
33	32	biimpcd	$$⊢\left(\exists x\left(x=u\wedge y=v\right)\to \exists x\neg \forall xx=y\right)\to \left(\left(\exists x\neg \forall xx=y\leftrightarrow \neg \forall xx=y\right)\to \left(\exists x\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\right)$$
34	29 31 33	e10	$$⊢\left(u\ne v\to \left(\exists x\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\right)$$
35	34	gen11	$$⊢\left(u\ne v\to \forall y\left(\exists x\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\right)$$
36		exim	$$⊢\forall y\left(\exists x\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\to \left(\exists y\exists x\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)$$
37	35 36	e1a	$$⊢\left(u\ne v\to \left(\exists y\exists x\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)\right)$$
38		excom	$$⊢\exists x\exists y\left(x=u\wedge y=v\right)\leftrightarrow \exists y\exists x\left(x=u\wedge y=v\right)$$
39		imbi1	$$⊢\left(\exists x\exists y\left(x=u\wedge y=v\right)\leftrightarrow \exists y\exists x\left(x=u\wedge y=v\right)\right)\to \left(\left(\exists x\exists y\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)\leftrightarrow \left(\exists y\exists x\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)\right)$$
40	39	biimprcd	$$⊢\left(\exists y\exists x\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)\to \left(\left(\exists x\exists y\left(x=u\wedge y=v\right)\leftrightarrow \exists y\exists x\left(x=u\wedge y=v\right)\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)\right)$$
41	37 38 40	e10	$$⊢\left(u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)\right)$$
42		hbnae	$$⊢\neg \forall xx=y\to \forall y\neg \forall xx=y$$
43	42	eximi	$$⊢\exists y\neg \forall xx=y\to \exists y\forall y\neg \forall xx=y$$
44		nfa1	$$⊢Ⅎy\forall y\neg \forall xx=y$$
45	44	19.9	$$⊢\exists y\forall y\neg \forall xx=y\leftrightarrow \forall y\neg \forall xx=y$$
46	43 45	sylib	$$⊢\exists y\neg \forall xx=y\to \forall y\neg \forall xx=y$$
47		sp	$$⊢\forall y\neg \forall xx=y\to \neg \forall xx=y$$
48	46 47	syl	$$⊢\exists y\neg \forall xx=y\to \neg \forall xx=y$$
49		imim1	$$⊢\left(\exists x\exists y\left(x=u\wedge y=v\right)\to \exists y\neg \forall xx=y\right)\to \left(\left(\exists y\neg \forall xx=y\to \neg \forall xx=y\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\right)$$
50	41 48 49	e10	$$⊢\left(u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\right)$$
51		orc	$$⊢\neg \forall xx=y\to \left(\neg \forall xx=y\vee u=v\right)$$
52	51	imim2i	$$⊢\left(\exists x\exists y\left(x=u\wedge y=v\right)\to \neg \forall xx=y\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
53	50 52	e1a	$$⊢\left(u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)$$
54	53	in1	$$⊢u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
55		idn1	$$⊢\left(u=v\to u=v\right)$$
56		ax-1	$$⊢u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to u=v\right)$$
57	55 56	e1a	$$⊢\left(u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to u=v\right)\right)$$
58		olc	$$⊢u=v\to \left(\neg \forall xx=y\vee u=v\right)$$
59	58	imim2i	$$⊢\left(\exists x\exists y\left(x=u\wedge y=v\right)\to u=v\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
60	57 59	e1a	$$⊢\left(u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)$$
61	60	in1	$$⊢u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)$$
62		exmidne	$$⊢\left(u=v\vee u\ne v\right)$$
63		jao	$$⊢\left(u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)\to \left(\left(u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)\to \left(\left(u=v\vee u\ne v\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)\right)$$
64	63	com12	$$⊢\left(u\ne v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)\to \left(\left(u=v\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)\to \left(\left(u=v\vee u\ne v\right)\to \left(\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)\right)\right)\right)$$
65	54 61 62 64	e000	$$⊢\exists x\exists y\left(x=u\wedge y=v\right)\to \left(\neg \forall xx=y\vee u=v\right)$$
66	7 65	impbii	$$⊢\left(\neg \forall xx=y\vee u=v\right)\leftrightarrow \exists x\exists y\left(x=u\wedge y=v\right)$$