Theorem reuxfr1ds

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Use reuhypd to eliminate the second hypothesis. (Contributed by NM, 16-Jan-2012)

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

Proof

Step	Hyp	Ref	Expression
1		reuxfr1ds.1	|- ( ( ph /\ y e. C ) -> A e. B )
2		reuxfr1ds.2	|- ( ( ph /\ x e. B ) -> E! y e. C x = A )
3		reuxfr1ds.3	|- ( x = A -> ( ps <-> ch ) )
4	3	adantl	|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
5	1 2 4	reuxfr1d	|- ( ph -> ( E! x e. B ps <-> E! y e. C ch ) )