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

Metamath Proof Explorer

Theorem eusv1

Description: Two ways to express single-valuedness of a class expression A ( x ) . (Contributed by NM, 14-Oct-2010)

Ref Expression
Assertion eusv1 
|- ( E! y A. x y = A <-> E. y A. x y = A )

Proof

Step Hyp Ref Expression
1 sp 
 |-  ( A. x y = A -> y = A )
2 sp 
 |-  ( A. x z = A -> z = A )
3 eqtr3 
 |-  ( ( y = A /\ z = A ) -> y = z )
4 1 2 3 syl2an 
 |-  ( ( A. x y = A /\ A. x z = A ) -> y = z )
5 4 gen2 
 |-  A. y A. z ( ( A. x y = A /\ A. x z = A ) -> y = z )
6 eqeq1 
 |-  ( y = z -> ( y = A <-> z = A ) )
7 6 albidv 
 |-  ( y = z -> ( A. x y = A <-> A. x z = A ) )
8 7 eu4 
 |-  ( E! y A. x y = A <-> ( E. y A. x y = A /\ A. y A. z ( ( A. x y = A /\ A. x z = A ) -> y = z ) ) )
9 5 8 mpbiran2 
 |-  ( E! y A. x y = A <-> E. y A. x y = A )