Metamath Proof Explorer

Theorem ax6e2eqVD

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

1:: |- (. A. x x = y ->. A. x x = y ).
2:: |- (. A. x x = y ,. x = u ->. x = u ).
3:1: |- (. A. x x = y ->. x = y ).
4:2,3: |- (. A. x x = y ,. x = u ->. y = u ).
5:2,4: |- (. A. x x = y ,. x = u ->. ( x = u /\ y = u ) ).
6:5: |- (. A. x x = y ->. ( x = u -> ( x = u /\ y = u ) ) ).
7:6: |- ( A. x x = y -> ( x = u -> ( x = u /\ y = u ) ) )
8:7: |- ( A. x A. x x = y -> A. x ( x = u -> ( x = u /\ y = u ) ) )
9:: |- ( A. x x = y <-> A. x A. x x = y )
10:8,9: |- ( A. x x = y -> A. x ( x = u -> ( x = u /\ y = u ) ) )
11:1,10: |- (. A. x x = y ->. A. x ( x = u -> ( x = u /\ y = u ) ) ).
12:11: |- (. A. x x = y ->. ( E. x x = u -> E. x ( x = u /\ y = u ) ) ).
13:: |- E. x x = u
14:13,12: |- (. A. x x = y ->. E. x ( x = u /\ y = u ) ).
140:14: |- ( A. x x = y -> E. x ( x = u /\ y = u ) )
141:140: |- ( A. x x = y -> A. x E. x ( x = u /\ y = u ) )
15:1,141: |- (. A. x x = y ->. A. x E. x ( x = u /\ y = u ) ).
16:1,15: |- (. A. x x = y ->. A. y E. x ( x = u /\ y = u ) ).
17:16: |- (. A. x x = y ->. E. y E. x ( x = u /\ y = u ) ).
18:17: |- (. A. x x = y ->. E. x E. y ( x = u /\ y = u ) ).
19:: |- (. u = v ->. u = v ).
20:: |- (. u = v ,. ( x = u /\ y = u ) ->. ( x = u /\ y = u ) ).
21:20: |- (. u = v ,. ( x = u /\ y = u ) ->. y = u ).
22:19,21: |- (. u = v ,. ( x = u /\ y = u ) ->. y = v ).
23:20: |- (. u = v ,. ( x = u /\ y = u ) ->. x = u ).
24:22,23: |- (. u = v ,. ( x = u /\ y = u ) ->. ( x = u /\ y = v ) ).
25:24: |- (. u = v ->. ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) ).
26:25: |- (. u = v ->. A. y ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) ).
27:26: |- (. u = v ->. ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) ).
28:27: |- (. u = v ->. A. x ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) ).
29:28: |- (. u = v ->. ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) ).
30:29: |- ( u = v -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) )
31:18,30: |- (. A. x x = y ->. ( u = v -> E. x E. y ( x = u /\ y = v ) ) ).
qed:31: |- ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )

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

Proof

Step Hyp Ref Expression
1 idn1 
 |-  (. A. x x = y ->. A. x x = y ).
2 ax6ev 
 |-  E. x x = u
3 hba1 
 |-  ( A. x x = y -> A. x A. x x = y )
4 sp 
 |-  ( A. x A. x x = y -> A. x x = y )
5 3 4 impbii 
 |-  ( A. x x = y <-> A. x A. x x = y )
6 idn2 
 |-  (. A. x x = y ,. x = u ->. x = u ).
7 sp 
 |-  ( A. x x = y -> x = y )
8 1 7 e1a 
 |-  (. A. x x = y ->. x = y ).
9 ax7 
 |-  ( x = y -> ( x = u -> y = u ) )
10 9 com12 
 |-  ( x = u -> ( x = y -> y = u ) )
11 6 8 10 e21 
 |-  (. A. x x = y ,. x = u ->. y = u ).
12 pm3.2 
 |-  ( x = u -> ( y = u -> ( x = u /\ y = u ) ) )
13 6 11 12 e22 
 |-  (. A. x x = y ,. x = u ->. ( x = u /\ y = u ) ).
14 13 in2 
 |-  (. A. x x = y ->. ( x = u -> ( x = u /\ y = u ) ) ).
15 14 in1 
 |-  ( A. x x = y -> ( x = u -> ( x = u /\ y = u ) ) )
16 15 alimi 
 |-  ( A. x A. x x = y -> A. x ( x = u -> ( x = u /\ y = u ) ) )
17 5 16 sylbi 
 |-  ( A. x x = y -> A. x ( x = u -> ( x = u /\ y = u ) ) )
18 1 17 e1a 
 |-  (. A. x x = y ->. A. x ( x = u -> ( x = u /\ y = u ) ) ).
19 exim 
 |-  ( A. x ( x = u -> ( x = u /\ y = u ) ) -> ( E. x x = u -> E. x ( x = u /\ y = u ) ) )
20 18 19 e1a 
 |-  (. A. x x = y ->. ( E. x x = u -> E. x ( x = u /\ y = u ) ) ).
21 pm2.27 
 |-  ( E. x x = u -> ( ( E. x x = u -> E. x ( x = u /\ y = u ) ) -> E. x ( x = u /\ y = u ) ) )
22 2 20 21 e01 
 |-  (. A. x x = y ->. E. x ( x = u /\ y = u ) ).
23 22 in1 
 |-  ( A. x x = y -> E. x ( x = u /\ y = u ) )
24 23 axc4i 
 |-  ( A. x x = y -> A. x E. x ( x = u /\ y = u ) )
25 1 24 e1a 
 |-  (. A. x x = y ->. A. x E. x ( x = u /\ y = u ) ).
26 axc11 
 |-  ( A. x x = y -> ( A. x E. x ( x = u /\ y = u ) -> A. y E. x ( x = u /\ y = u ) ) )
27 1 25 26 e11 
 |-  (. A. x x = y ->. A. y E. x ( x = u /\ y = u ) ).
28 19.2 
 |-  ( A. y E. x ( x = u /\ y = u ) -> E. y E. x ( x = u /\ y = u ) )
29 27 28 e1a 
 |-  (. A. x x = y ->. E. y E. x ( x = u /\ y = u ) ).
30 excomim 
 |-  ( E. y E. x ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = u ) )
31 29 30 e1a 
 |-  (. A. x x = y ->. E. x E. y ( x = u /\ y = u ) ).
32 idn1 
 |-  (. u = v ->. u = v ).
33 idn2 
 |-  (. u = v ,. ( x = u /\ y = u ) ->. ( x = u /\ y = u ) ).
34 simpr 
 |-  ( ( x = u /\ y = u ) -> y = u )
35 33 34 e2 
 |-  (. u = v ,. ( x = u /\ y = u ) ->. y = u ).
36 equtrr 
 |-  ( u = v -> ( y = u -> y = v ) )
37 32 35 36 e12 
 |-  (. u = v ,. ( x = u /\ y = u ) ->. y = v ).
38 simpl 
 |-  ( ( x = u /\ y = u ) -> x = u )
39 33 38 e2 
 |-  (. u = v ,. ( x = u /\ y = u ) ->. x = u ).
40 pm3.21 
 |-  ( y = v -> ( x = u -> ( x = u /\ y = v ) ) )
41 37 39 40 e22 
 |-  (. u = v ,. ( x = u /\ y = u ) ->. ( x = u /\ y = v ) ).
42 41 in2 
 |-  (. u = v ->. ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) ).
43 42 gen11 
 |-  (. u = v ->. A. y ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) ).
44 exim 
 |-  ( A. y ( ( x = u /\ y = u ) -> ( x = u /\ y = v ) ) -> ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) )
45 43 44 e1a 
 |-  (. u = v ->. ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) ).
46 45 gen11 
 |-  (. u = v ->. A. x ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) ).
47 exim 
 |-  ( A. x ( E. y ( x = u /\ y = u ) -> E. y ( x = u /\ y = v ) ) -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) )
48 46 47 e1a 
 |-  (. u = v ->. ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) ).
49 48 in1 
 |-  ( u = v -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) )
50 pm2.04 
 |-  ( ( u = v -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) ) -> ( E. x E. y ( x = u /\ y = u ) -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) )
51 50 com12 
 |-  ( E. x E. y ( x = u /\ y = u ) -> ( ( u = v -> ( E. x E. y ( x = u /\ y = u ) -> E. x E. y ( x = u /\ y = v ) ) ) -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) ) )
52 31 49 51 e10 
 |-  (. A. x x = y ->. ( u = v -> E. x E. y ( x = u /\ y = v ) ) ).
53 52 in1 
 |-  ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )