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 x x = y u = v x y x = u y = v

Proof

Step Hyp Ref Expression
1 idn1 x x = y x x = y
2 ax6ev x x = u
3 hba1 x x = y x x x = y
4 sp x x x = y x x = y
5 3 4 impbii x x = y x x x = y
6 idn2 x x = y , x = u x = u
7 sp x x = y x = y
8 1 7 e1a 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 x x = y , x = u y = u
12 pm3.2 x = u y = u x = u y = u
13 6 11 12 e22 x x = y , x = u x = u y = u
14 13 in2 x x = y x = u x = u y = u
15 14 in1 x x = y x = u x = u y = u
16 15 alimi x x x = y x x = u x = u y = u
17 5 16 sylbi x x = y x x = u x = u y = u
18 1 17 e1a x x = y x x = u x = u y = u
19 exim x x = u x = u y = u x x = u x x = u y = u
20 18 19 e1a x x = y x x = u x x = u y = u
21 pm2.27 x x = u x x = u x x = u y = u x x = u y = u
22 2 20 21 e01 x x = y x x = u y = u
23 22 in1 x x = y x x = u y = u
24 23 axc4i x x = y x x x = u y = u
25 1 24 e1a x x = y x x x = u y = u
26 axc11 x x = y x x x = u y = u y x x = u y = u
27 1 25 26 e11 x x = y y x x = u y = u
28 19.2 y x x = u y = u y x x = u y = u
29 27 28 e1a x x = y y x x = u y = u
30 excomim y x x = u y = u x y x = u y = u
31 29 30 e1a x x = y x 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 y x = u y = u x = u y = v
44 exim y x = u y = u x = u y = v y x = u y = u y x = u y = v
45 43 44 e1a u = v y x = u y = u y x = u y = v
46 45 gen11 u = v x y x = u y = u y x = u y = v
47 exim x y x = u y = u y x = u y = v x y x = u y = u x y x = u y = v
48 46 47 e1a u = v x y x = u y = u x y x = u y = v
49 48 in1 u = v x y x = u y = u x y x = u y = v
50 pm2.04 u = v x y x = u y = u x y x = u y = v x y x = u y = u u = v x y x = u y = v
51 50 com12 x y x = u y = u u = v x y x = u y = u x y x = u y = v u = v x y x = u y = v
52 31 49 51 e10 x x = y u = v x y x = u y = v
53 52 in1 x x = y u = v x y x = u y = v