Theorem ax6e2ndeqVD 39145

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

1::	|- (. u =/= v ->. u =/= v ).
2::	|- (. u =/= v ,. ( x = u /\ y = v ) ->. ( x = u /\ y = v ) ).
3:2:	|- (. u =/= v ,. ( x = u /\ y = v ) ->. x = u ).
4:1,3:	|- (. u =/= v ,. ( x = u /\ y = v ) ->. x =/= v ).
5:2:	|- (. u =/= v ,. ( x = u /\ y = v ) ->. y = v ).
6:4,5:	|- (. u =/= v ,. ( x = u /\ y = v ) ->. x =/= y ).
7::	|- ( A. x x = y -> x = y )
8:7:	|- ( -. x = y -> -. A. x x = y )
9::	|- ( -. x = y <-> x =/= y )
10:8,9:	|- ( x =/= y -> -. A. x x = y )
11:6,10:	|- (. u =/= v ,. ( x = u /\ y = v ) ->. -. A. x x = y ).
12:11:	|- (. u =/= v ->. ( ( x = u /\ y = v ) -> -. A. x x = y ) ).
13:12:	|- (. u =/= v ->. A. x ( ( x = u /\ y = v ) -> -. A. x x = y ) ).
14:13:	|- (. u =/= v ->. ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) ).
15::	|- ( -. A. x x = y -> A. x -. A. x x = y )
19:15:	|- ( E. x -. A. x x = y <-> -. A. x x = y )
20:14,19:	|- (. u =/= v ->. ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) ).
21:20:	|- (. u =/= v ->. A. y ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) ).
22:21:	|- (. u =/= v ->. ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) ).
23::	|- ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) )
24:22,23:	|- (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) ).
25::	|- ( -. A. x x = y -> A. y -. A. x x = y )
26:25:	|- ( E. y -. A. x x = y -> E. y A. y -. A. x x = y )
260::	|- ( A. y -. A. x x = y -> A. y A. y -. A. x x = y )
27:260:	|- ( E. y A. y -. A. x x = y <-> A. y -. A. x x = y )
270:26,27:	|- ( E. y -. A. x x = y -> A. y -. A. x x = y )
28::	|- ( A. y -. A. x x = y -> -. A. x x = y )
29:270,28:	|- ( E. y -. A. x x = y -> -. A. x x = y )
30:24,29:	|- (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) ).
31:30:	|- (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ).
32:31:	|- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
33::	|- (. u = v ->. u = v ).
34:33:	|- (. u = v ->. ( E. x E. y ( x = u /\ y = v ) -> u = v ) ).
35:34:	|- (. u = v ->. ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ).
36:35:	|- ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
37::	|- ( u = v \/ u =/= v )
38:32,36,37:	|- ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) )
39::	|- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
40::	|- ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )
41:40:	|- ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
42::	|- ( A. x x = y \/ -. A. x x = y )
43:39,41,42:	|- ( u = v -> E. x E. y ( x = u /\ y = v ) )
44:40,43:	|- ( ( -. A. x x = y \/ u = v ) -> E. x E. y ( x = u /\ y = v ) )
qed:38,44:	|- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )

Assertion

Ref	Expression
ax6e2ndeqVD	|- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )

Distinct variable groups:   x, u   y, u   x, v   y, v

Proof of Theorem ax6e2ndeqVD

Step	Hyp	Ref	Expression
1		ax6e2nd 38774	. . 3 |- ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )
2		ax6e2eq 38773	. . . 4 |- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
3	1	a1d 25	. . . 4 |- ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
4		exmid 431	. . . 4 |- ( A. x x = y \/ -. A. x x = y )
5		jao 534	. . . 4 |- ( ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) -> ( ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) -> ( ( A. x x = y \/ -. A. x x = y ) -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) ) )
6	2, 3, 4, 5	e000 38994	. . 3 |- ( u = v -> E. x E. y ( x = u /\ y = v ) )
7	1, 6	jaoi 394	. 2 |- ( ( -. A. x x = y \/ u = v ) -> E. x E. y ( x = u /\ y = v ) )
8		idn1 38790	. . . . . . . . . . . . . . . 16 |- (. u =/= v ->. u =/= v ).
9		idn2 38838	. . . . . . . . . . . . . . . . 17 |- (. u =/= v ,. ( x = u /\ y = v ) ->. ( x = u /\ y = v ) ).
10		simpl 473	. . . . . . . . . . . . . . . . 17 |- ( ( x = u /\ y = v ) -> x = u )
11	9, 10	e2 38856	. . . . . . . . . . . . . . . 16 |- (. u =/= v ,. ( x = u /\ y = v ) ->. x = u ).
12		neeq1 2856	. . . . . . . . . . . . . . . . 17 |- ( x = u -> ( x =/= v <-> u =/= v ) )
13	12	biimprcd 240	. . . . . . . . . . . . . . . 16 |- ( u =/= v -> ( x = u -> x =/= v ) )
14	8, 11, 13	e12 38951	. . . . . . . . . . . . . . 15 |- (. u =/= v ,. ( x = u /\ y = v ) ->. x =/= v ).
15		simpr 477	. . . . . . . . . . . . . . . 16 |- ( ( x = u /\ y = v ) -> y = v )
16	9, 15	e2 38856	. . . . . . . . . . . . . . 15 |- (. u =/= v ,. ( x = u /\ y = v ) ->. y = v ).
17		neeq2 2857	. . . . . . . . . . . . . . . 16 |- ( y = v -> ( x =/= y <-> x =/= v ) )
18	17	biimprcd 240	. . . . . . . . . . . . . . 15 |- ( x =/= v -> ( y = v -> x =/= y ) )
19	14, 16, 18	e22 38896	. . . . . . . . . . . . . 14 |- (. u =/= v ,. ( x = u /\ y = v ) ->. x =/= y ).
20		df-ne 2795	. . . . . . . . . . . . . . . 16 |- ( x =/= y <-> -. x = y )
21	20	bicomi 214	. . . . . . . . . . . . . . 15 |- ( -. x = y <-> x =/= y )
22		sp 2053	. . . . . . . . . . . . . . . 16 |- ( A. x x = y -> x = y )
23	22	con3i 150	. . . . . . . . . . . . . . 15 |- ( -. x = y -> -. A. x x = y )
24	21, 23	sylbir 225	. . . . . . . . . . . . . 14 |- ( x =/= y -> -. A. x x = y )
25	19, 24	e2 38856	. . . . . . . . . . . . 13 |- (. u =/= v ,. ( x = u /\ y = v ) ->. -. A. x x = y ).
26	25	in2 38830	. . . . . . . . . . . 12 |- (. u =/= v ->. ( ( x = u /\ y = v ) -> -. A. x x = y ) ).
27	26	gen11 38841	. . . . . . . . . . 11 |- (. u =/= v ->. A. x ( ( x = u /\ y = v ) -> -. A. x x = y ) ).
28		exim 1761	. . . . . . . . . . 11 |- ( A. x ( ( x = u /\ y = v ) -> -. A. x x = y ) -> ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) )
29	27, 28	e1a 38852	. . . . . . . . . 10 |- (. u =/= v ->. ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) ).
30		nfnae 2318	. . . . . . . . . . 11 |- F/ x -. A. x x = y
31	30	19.9 2072	. . . . . . . . . 10 |- ( E. x -. A. x x = y <-> -. A. x x = y )
32		imbi2 338	. . . . . . . . . . 11 |- ( ( E. x -. A. x x = y <-> -. A. x x = y ) -> ( ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) <-> ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) ) )
33	32	biimpcd 239	. . . . . . . . . 10 |- ( ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) -> ( ( E. x -. A. x x = y <-> -. A. x x = y ) -> ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) ) )
34	29, 31, 33	e10 38919	. . . . . . . . 9 |- (. u =/= v ->. ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) ).
35	34	gen11 38841	. . . . . . . 8 |- (. u =/= v ->. A. y ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) ).
36		exim 1761	. . . . . . . 8 |- ( A. y ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) -> ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) )
37	35, 36	e1a 38852	. . . . . . 7 |- (. u =/= v ->. ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) ).
38		excom 2042	. . . . . . 7 |- ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) )
39		imbi1 337	. . . . . . . 8 |- ( ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) ) -> ( ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) <-> ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) ) )
40	39	biimprcd 240	. . . . . . 7 |- ( ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) -> ( ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) ) -> ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) ) )
41	37, 38, 40	e10 38919	. . . . . 6 |- (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) ).
42		hbnae 2317	. . . . . . . . 9 |- ( -. A. x x = y -> A. y -. A. x x = y )
43	42	eximi 1762	. . . . . . . 8 |- ( E. y -. A. x x = y -> E. y A. y -. A. x x = y )
44		nfa1 2028	. . . . . . . . 9 |- F/ y A. y -. A. x x = y
45	44	19.9 2072	. . . . . . . 8 |- ( E. y A. y -. A. x x = y <-> A. y -. A. x x = y )
46	43, 45	sylib 208	. . . . . . 7 |- ( E. y -. A. x x = y -> A. y -. A. x x = y )
47		sp 2053	. . . . . . 7 |- ( A. y -. A. x x = y -> -. A. x x = y )
48	46, 47	syl 17	. . . . . 6 |- ( E. y -. A. x x = y -> -. A. x x = y )
49		imim1 83	. . . . . 6 |- ( ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) -> ( ( E. y -. A. x x = y -> -. A. x x = y ) -> ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) ) )
50	41, 48, 49	e10 38919	. . . . 5 |- (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) ).
51		orc 400	. . . . . 6 |- ( -. A. x x = y -> ( -. A. x x = y \/ u = v ) )
52	51	imim2i 16	. . . . 5 |- ( ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
53	50, 52	e1a 38852	. . . 4 |- (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ).
54	53	in1 38787	. . 3 |- ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
55		idn1 38790	. . . . . 6 |- (. u = v ->. u = v ).
56		ax-1 6	. . . . . 6 |- ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> u = v ) )
57	55, 56	e1a 38852	. . . . 5 |- (. u = v ->. ( E. x E. y ( x = u /\ y = v ) -> u = v ) ).
58		olc 399	. . . . . 6 |- ( u = v -> ( -. A. x x = y \/ u = v ) )
59	58	imim2i 16	. . . . 5 |- ( ( E. x E. y ( x = u /\ y = v ) -> u = v ) -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
60	57, 59	e1a 38852	. . . 4 |- (. u = v ->. ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ).
61	60	in1 38787	. . 3 |- ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
62		exmidne 2804	. . 3 |- ( u = v \/ u =/= v )
63		jao 534	. . . 4 |- ( ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ) -> ( ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ) -> ( ( u = v \/ u =/= v ) -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ) ) )
64	63	com12 32	. . 3 |- ( ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ) -> ( ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ) -> ( ( u = v \/ u =/= v ) -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ) ) )
65	54, 61, 62, 64	e000 38994	. 2 |- ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) )
66	7, 65	impbii 199	1 |- ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   \/ wo 383   /\ wa 384   A.wal 1481   = wceq 1483   E.wex 1704   =/= wne 2794

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-ne 2795  df-v 3202  df-vd1 38786  df-vd2 38794

This theorem is referenced by: (None)