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 ) )