Theorem reuxfr

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . (Contributed by NM, 14-Nov-2004) (Revised by NM, 16-Jun-2017)

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

Proof

Step	Hyp	Ref	Expression
1		reuxfr.1	|- ( y e. C -> A e. B )
2		reuxfr.2	|- ( x e. B -> E* y e. C x = A )
3	1	adantl	|- ( ( T. /\ y e. C ) -> A e. B )
4	2	adantl	|- ( ( T. /\ x e. B ) -> E* y e. C x = A )
5	3 4	reuxfrd	|- ( T. -> ( E! x e. B E. y e. C ( x = A /\ ph ) <-> E! y e. C ph ) )
6	5	mptru	|- ( E! x e. B E. y e. C ( x = A /\ ph ) <-> E! y e. C ph )