Metamath Proof Explorer

Theorem wl-exeq

Description: The semantics of E. x y = z . (Contributed by Wolf Lammen, 27-Apr-2018)

Ref Expression
Assertion wl-exeq 
|- ( E. x y = z <-> ( y = z \/ A. x x = y \/ A. x x = z ) )

Proof

Step Hyp Ref Expression
1 nfeqf 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> F/ x y = z )
2 1 19.9d 
 |-  ( ( -. A. x x = y /\ -. A. x x = z ) -> ( E. x y = z -> y = z ) )
3 2 impancom 
 |-  ( ( -. A. x x = y /\ E. x y = z ) -> ( -. A. x x = z -> y = z ) )
4 3 orrd 
 |-  ( ( -. A. x x = y /\ E. x y = z ) -> ( A. x x = z \/ y = z ) )
5 4 expcom 
 |-  ( E. x y = z -> ( -. A. x x = y -> ( A. x x = z \/ y = z ) ) )
6 5 orrd 
 |-  ( E. x y = z -> ( A. x x = y \/ ( A. x x = z \/ y = z ) ) )
7 3orass 
 |-  ( ( A. x x = y \/ A. x x = z \/ y = z ) <-> ( A. x x = y \/ ( A. x x = z \/ y = z ) ) )
8 6 7 sylibr 
 |-  ( E. x y = z -> ( A. x x = y \/ A. x x = z \/ y = z ) )
9 3orrot 
 |-  ( ( y = z \/ A. x x = y \/ A. x x = z ) <-> ( A. x x = y \/ A. x x = z \/ y = z ) )
10 8 9 sylibr 
 |-  ( E. x y = z -> ( y = z \/ A. x x = y \/ A. x x = z ) )
11 19.8a 
 |-  ( y = z -> E. x y = z )
12 ax6e 
 |-  E. x x = z
13 ax7 
 |-  ( x = y -> ( x = z -> y = z ) )
14 13 com12 
 |-  ( x = z -> ( x = y -> y = z ) )
15 12 14 eximii 
 |-  E. x ( x = y -> y = z )
16 15 19.35i 
 |-  ( A. x x = y -> E. x y = z )
17 ax6e 
 |-  E. x x = y
18 17 13 eximii 
 |-  E. x ( x = z -> y = z )
19 18 19.35i 
 |-  ( A. x x = z -> E. x y = z )
20 11 16 19 3jaoi 
 |-  ( ( y = z \/ A. x x = y \/ A. x x = z ) -> E. x y = z )
21 10 20 impbii 
 |-  ( E. x y = z <-> ( y = z \/ A. x x = y \/ A. x x = z ) )