Metamath Proof Explorer

Theorem eusv4

Description: Two ways to express single-valuedness of a class expression B ( y ) . (Contributed by NM, 27-Oct-2010)

Ref Expression
Hypothesis eusv4.1 
|- B e. _V
Assertion eusv4 
|- ( E! x E. y e. A x = B <-> E! x A. y e. A x = B )

Proof

Step Hyp Ref Expression
1 eusv4.1 
 |-  B e. _V
2 reusv2lem3 
 |-  ( A. y e. A B e. _V -> ( E! x E. y e. A x = B <-> E! x A. y e. A x = B ) )
3 1 a1i 
 |-  ( y e. A -> B e. _V )
4 2 3 mprg 
 |-  ( E! x E. y e. A x = B <-> E! x A. y e. A x = B )