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 ) ) |
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 ) ) |