Metamath Proof Explorer

Theorem ax6e2ndALT

Description: If at least two sets exist ( dtru ), then the same is true expressed in an alternate form similar to the form of ax6e . The proof is derived by completeusersproof.c from User's Proof in VirtualDeductionProofs.txt. The User's Proof in html format is displayed in ax6e2ndVD . (Contributed by Alan Sare, 11-Sep-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ax6e2ndALT 
|- ( -. 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 17 a1i 
 |-  ( ( z = y -> z = y ) -> ( z = y -> ( z = v <-> y = v ) ) )
19 16 18 ax-mp 
 |-  ( 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 pm3.35 
 |-  ( ( 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 sylancr 
 |-  ( -. 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 ) )