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