This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ax6e2ndVD

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

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

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

Proof

Step Hyp Ref Expression
1 vex 
 |-  u e. _V
2 ax6e 
 |-  E. y y = v
3 1 2 pm3.2i 
 |-  ( u e. _V /\ E. y y = v )
4 19.42v 
 |-  ( E. y ( u e. _V /\ y = v ) <-> ( u e. _V /\ E. y y = v ) )
5 4 biimpri 
 |-  ( ( u e. _V /\ E. y y = v ) -> E. y ( u e. _V /\ y = v ) )
6 3 5 e0a 
 |-  E. y ( u e. _V /\ y = v )
7 isset 
 |-  ( u e. _V <-> E. x x = u )
8 7 anbi1i 
 |-  ( ( u e. _V /\ y = v ) <-> ( E. x x = u /\ y = v ) )
9 8 exbii 
 |-  ( E. y ( u e. _V /\ y = v ) <-> E. y ( E. x x = u /\ y = v ) )
10 6 9 mpbi 
 |-  E. y ( E. x x = u /\ y = v )
11 idn1 
 |-  (. -. A. x x = y ->. -. A. x x = y ).
12 hbnae 
 |-  ( -. A. x x = y -> A. y -. A. x x = y )
13 hbn1 
 |-  ( -. A. x x = y -> A. x -. A. x x = y )
14 ax-5 
 |-  ( z = v -> A. x z = v )
15 ax-5 
 |-  ( y = v -> A. z y = v )
16 idn1 
 |-  (. z = y ->. z = y ).
17 equequ1 
 |-  ( z = y -> ( z = v <-> y = v ) )
18 16 17 e1a 
 |-  (. z = y ->. ( z = v <-> y = v ) ).
19 18 in1 
 |-  ( z = y -> ( z = v <-> y = v ) )
20 14 15 19 dvelimh 
 |-  ( -. A. x x = y -> ( y = v -> A. x y = v ) )
21 11 20 e1a 
 |-  (. -. A. x x = y ->. ( y = v -> A. x y = v ) ).
22 21 in1 
 |-  ( -. A. x x = y -> ( y = v -> A. x y = v ) )
23 22 alimi 
 |-  ( A. x -. A. x x = y -> A. x ( y = v -> A. x y = v ) )
24 13 23 syl 
 |-  ( -. A. x x = y -> A. x ( y = v -> A. x y = v ) )
25 11 24 e1a 
 |-  (. -. A. x x = y ->. A. x ( y = v -> A. x y = v ) ).
26 19.41rg 
 |-  ( A. x ( y = v -> A. x y = v ) -> ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
27 25 26 e1a 
 |-  (. -. A. x x = y ->. ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) ).
28 27 in1 
 |-  ( -. A. x x = y -> ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
29 28 alimi 
 |-  ( A. y -. A. x x = y -> A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
30 12 29 syl 
 |-  ( -. A. x x = y -> A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
31 11 30 e1a 
 |-  (. -. A. x x = y ->. A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) ).
32 exim 
 |-  ( A. y ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) -> ( E. y ( E. x x = u /\ y = v ) -> E. y E. x ( x = u /\ y = v ) ) )
33 31 32 e1a 
 |-  (. -. A. x x = y ->. ( E. y ( E. x x = u /\ y = v ) -> E. y E. x ( x = u /\ y = v ) ) ).
34 pm2.27 
 |-  ( E. y ( E. x x = u /\ y = v ) -> ( ( E. y ( E. x x = u /\ y = v ) -> E. y E. x ( x = u /\ y = v ) ) -> E. y E. x ( x = u /\ y = v ) ) )
35 10 33 34 e01 
 |-  (. -. A. x x = y ->. E. y E. x ( x = u /\ y = v ) ).
36 excomim 
 |-  ( E. y E. x ( x = u /\ y = v ) -> E. x E. y ( x = u /\ y = v ) )
37 35 36 e1a 
 |-  (. -. A. x x = y ->. E. x E. y ( x = u /\ y = v ) ).
38 37 in1 
 |-  ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )