Metamath Proof Explorer

Theorem ax6e2ndeq

Description: "At least two sets exist" expressed in the form of dtru is logically equivalent to the same expressed in a form similar to ax6e if dtru is false implies u = v . ax6e2ndeq is derived from ax6e2ndeqVD . (Contributed by Alan Sare, 25-Mar-2014) (Proof modification is discouraged.) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ax6e2nd 
 |-  ( -. A. x x = y -> E. x E. y ( x = u /\ y = v ) )
2 ax6e2eq 
 |-  ( A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
3 1 a1d 
 |-  ( -. A. x x = y -> ( u = v -> E. x E. y ( x = u /\ y = v ) ) )
4 2 3 pm2.61i 
 |-  ( u = v -> E. x E. y ( x = u /\ y = v ) )
5 1 4 jaoi 
 |-  ( ( -. A. x x = y \/ u = v ) -> E. x E. y ( x = u /\ y = v ) )
6 olc 
 |-  ( u = v -> ( -. A. x x = y \/ u = v ) )
7 6 a1d 
 |-  ( u = v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
8 excom 
 |-  ( E. x E. y ( x = u /\ y = v ) <-> E. y E. x ( x = u /\ y = v ) )
9 neeq1 
 |-  ( x = u -> ( x =/= v <-> u =/= v ) )
10 9 biimprcd 
 |-  ( u =/= v -> ( x = u -> x =/= v ) )
11 10 adantrd 
 |-  ( u =/= v -> ( ( x = u /\ y = v ) -> x =/= v ) )
12 simpr 
 |-  ( ( x = u /\ y = v ) -> y = v )
13 12 a1i 
 |-  ( u =/= v -> ( ( x = u /\ y = v ) -> y = v ) )
14 neeq2 
 |-  ( y = v -> ( x =/= y <-> x =/= v ) )
15 14 biimprcd 
 |-  ( x =/= v -> ( y = v -> x =/= y ) )
16 11 13 15 syl6c 
 |-  ( u =/= v -> ( ( x = u /\ y = v ) -> x =/= y ) )
17 sp 
 |-  ( A. x x = y -> x = y )
18 17 necon3ai 
 |-  ( x =/= y -> -. A. x x = y )
19 16 18 syl6 
 |-  ( u =/= v -> ( ( x = u /\ y = v ) -> -. A. x x = y ) )
20 19 eximdv 
 |-  ( u =/= v -> ( E. x ( x = u /\ y = v ) -> E. x -. A. x x = y ) )
21 nfnae 
 |-  F/ x -. A. x x = y
22 21 19.9 
 |-  ( E. x -. A. x x = y <-> -. A. x x = y )
23 20 22 syl6ib 
 |-  ( u =/= v -> ( E. x ( x = u /\ y = v ) -> -. A. x x = y ) )
24 23 eximdv 
 |-  ( u =/= v -> ( E. y E. x ( x = u /\ y = v ) -> E. y -. A. x x = y ) )
25 8 24 syl5bi 
 |-  ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> E. y -. A. x x = y ) )
26 nfnae 
 |-  F/ y -. A. x x = y
27 26 19.9 
 |-  ( E. y -. A. x x = y <-> -. A. x x = y )
28 25 27 syl6ib 
 |-  ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> -. A. x x = y ) )
29 orc 
 |-  ( -. A. x x = y -> ( -. A. x x = y \/ u = v ) )
30 28 29 syl6 
 |-  ( u =/= v -> ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) ) )
31 7 30 pm2.61ine 
 |-  ( E. x E. y ( x = u /\ y = v ) -> ( -. A. x x = y \/ u = v ) )
32 5 31 impbii 
 |-  ( ( -. A. x x = y \/ u = v ) <-> E. x E. y ( x = u /\ y = v ) )