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

Metamath Proof Explorer

Theorem ax6e2nd

Description: If at least two sets exist ( dtru ), then the same is true expressed in an alternate form similar to the form of ax6e . ax6e2nd is derived from ax6e2ndVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6e2nd 
|- ( -. 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 ax-mp 
 |-  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 id 
 |-  ( -. 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 id 
 |-  ( z = y -> z = y )
17 equequ1 
 |-  ( z = y -> ( z = v <-> y = v ) )
18 16 17 syl 
 |-  ( z = y -> ( z = v <-> y = v ) )
19 18 idiALT 
 |-  ( z = y -> ( z = v <-> y = v ) )
20 14 15 19 dvelimh 
 |-  ( -. A. x x = y -> ( y = v -> A. x y = v ) )
21 11 20 syl 
 |-  ( -. A. x x = y -> ( y = v -> A. x y = v ) )
22 21 idiALT 
 |-  ( -. 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 syl 
 |-  ( -. 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 syl 
 |-  ( -. A. x x = y -> ( ( E. x x = u /\ y = v ) -> E. x ( x = u /\ y = v ) ) )
28 27 idiALT 
 |-  ( -. 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 syl 
 |-  ( -. 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 syl 
 |-  ( -. 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 mpsyl 
 |-  ( -. 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 syl 
 |-  ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )
38 37 idiALT 
 |-  ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )