Metamath Proof Explorer


Theorem eusvobj1

Description: Specify the same object in two ways when class B ( y ) is single-valued. (Contributed by NM, 1-Nov-2010) (Proof shortened by Mario Carneiro, 19-Nov-2016)

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

Proof

Step Hyp Ref Expression
1 eusvobj1.1
 |-  B e. _V
2 nfeu1
 |-  F/ x E! x E. y e. A x = B
3 1 eusvobj2
 |-  ( E! x E. y e. A x = B -> ( E. y e. A x = B <-> A. y e. A x = B ) )
4 2 3 alrimi
 |-  ( E! x E. y e. A x = B -> A. x ( E. y e. A x = B <-> A. y e. A x = B ) )
5 iotabi
 |-  ( A. x ( E. y e. A x = B <-> A. y e. A x = B ) -> ( iota x E. y e. A x = B ) = ( iota x A. y e. A x = B ) )
6 4 5 syl
 |-  ( E! x E. y e. A x = B -> ( iota x E. y e. A x = B ) = ( iota x A. y e. A x = B ) )