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 )