Theorem reuhyp

Description: A theorem useful for eliminating the restricted existential uniqueness hypotheses in reuxfr1 . (Contributed by NM, 15-Nov-2004)

	Ref	Expression
Hypotheses	reuhyp.1	|- ( x e. C -> B e. C )
	reuhyp.2	|- ( ( x e. C /\ y e. C ) -> ( x = A <-> y = B ) )
Assertion	reuhyp	|- ( x e. C -> E! y e. C x = A )

Proof

Step	Hyp	Ref	Expression
1		reuhyp.1	|- ( x e. C -> B e. C )
2		reuhyp.2	|- ( ( x e. C /\ y e. C ) -> ( x = A <-> y = B ) )
3		tru	|- T.
4	1	adantl	|- ( ( T. /\ x e. C ) -> B e. C )
5	2	3adant1	|- ( ( T. /\ x e. C /\ y e. C ) -> ( x = A <-> y = B ) )
6	4 5	reuhypd	|- ( ( T. /\ x e. C ) -> E! y e. C x = A )
7	3 6	mpan	|- ( x e. C -> E! y e. C x = A )