Metamath Proof Explorer

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.)

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 ) )

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

Proof

Step Hyp Ref Expression
1 ax6e2nd 
 |-  ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )
2 ax6e2eq 
 |-  ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
3 1 a1d 
 |-  ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
4 exmid 
 |-  ( A. x x = y \/ -. A. x x = y )
5 jao 
 |-  ( ( 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 
 |-  ( u = v -> E. x E. y ( x = u /\ y = v ) )
7 1 6 jaoi 
 |-  ( ( -. A. x x = y \/ u = v ) -> E. x E. y ( x = u /\ y = v ) )
8 idn1 
 |-  (. u =/= v ->. u =/= v ).
9 idn2 
 |-  (. u =/= v ,. ( x = u /\ y = v ) ->. ( x = u /\ y = v ) ).
10 simpl 
 |-  ( ( x = u /\ y = v ) -> x = u )
11 9 10 e2 
 |-  (. u =/= v ,. ( x = u /\ y = v ) ->. x = u ).
12 neeq1 
 |-  ( x = u -> ( x =/= v <-> u =/= v ) )
13 12 biimprcd 
 |-  ( u =/= v -> ( x = u -> x =/= v ) )
14 8 11 13 e12 
 |-  (. u =/= v ,. ( x = u /\ y = v ) ->. x =/= v ).
15 simpr 
 |-  ( ( x = u /\ y = v ) -> y = v )
16 9 15 e2 
 |-  (. u =/= v ,. ( x = u /\ y = v ) ->. y = v ).
17 neeq2 
 |-  ( y = v -> ( x =/= y <-> x =/= v ) )
18 17 biimprcd 
 |-  ( x =/= v -> ( y = v -> x =/= y ) )
19 14 16 18 e22 
 |-  (. u =/= v ,. ( x = u /\ y = v ) ->. x =/= y ).
20 df-ne 
 |-  ( x =/= y <-> -. x = y )
21 20 bicomi 
 |-  ( -. x = y <-> x =/= y )
22 sp 
 |-  ( A. x x = y -> x = y )
23 22 con3i 
 |-  ( -. x = y -> -. A. x x = y )
24 21 23 sylbir 
 |-  ( x =/= y -> -. A. x x = y )
25 19 24 e2 
 |-  (. u =/= v ,. ( x = u /\ y = v ) ->. -. A. x x = y ).
26 25 in2 
 |-  (. u =/= v ->. ( ( x = u /\ y = v ) -> -. A. x x = y ) ).
27 26 gen11 
 |-  (. u =/= v ->. A. x ( ( x = u /\ y = v ) -> -. A. x x = y ) ).
28 exim 
 |-  ( 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 
 |-  (. u =/= v ->. ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) ).
30 nfnae 
 |-  F/ x -. A. x x = y
31 30 19.9 
 |-  ( E. x -. A. x x = y <-> -. A. x x = y )
32 imbi2 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  (. u =/= v ->. ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) ).
35 34 gen11 
 |-  (. u =/= v ->. A. y ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) ).
36 exim 
 |-  ( 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 
 |-  (. u =/= v ->. ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) ).
38 excom 
 |-  ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) )
39 imbi1 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) ).
42 hbnae 
 |-  ( -. A. x x = y -> A. y -. A. x x = y )
43 42 eximi 
 |-  ( E. y -. A. x x = y -> E. y A. y -. A. x x = y )
44 nfa1 
 |-  F/ y A. y -. A. x x = y
45 44 19.9 
 |-  ( E. y A. y -. A. x x = y <-> A. y -. A. x x = y )
46 43 45 sylib 
 |-  ( E. y -. A. x x = y -> A. y -. A. x x = y )
47 sp 
 |-  ( A. y -. A. x x = y -> -. A. x x = y )
48 46 47 syl 
 |-  ( E. y -. A. x x = y -> -. A. x x = y )
49 imim1 
 |-  ( ( 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 
 |-  (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) ).
51 orc 
 |-  ( -. A. x x = y -> ( -. A. x x = y \/ u = v ) )
52 51 imim2i 
 |-  ( ( 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 
 |-  (. u =/= v ->. ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ).
54 53 in1 
 |-  ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
55 idn1 
 |-  (. u = v ->. u = v ).
56 ax-1 
 |-  ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> u = v ) )
57 55 56 e1a 
 |-  (. u = v ->. ( E. x E. y ( x = u /\ y = v ) -> u = v ) ).
58 olc 
 |-  ( u = v -> ( -. A. x x = y \/ u = v ) )
59 58 imim2i 
 |-  ( ( 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 
 |-  (. u = v ->. ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) ).
61 60 in1 
 |-  ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
62 exmidne 
 |-  ( u = v \/ u =/= v )
63 jao 
 |-  ( ( 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 
 |-  ( ( 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 
 |-  ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) )
66 7 65 impbii 
 |-  ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )