Theorem rexxfr

Description: Transfer existence from a variable x to another variable y contained in expression A . (Contributed by NM, 10-Jun-2005) (Revised by Mario Carneiro, 15-Aug-2014)

	Ref	Expression
Hypotheses	ralxfr.1	|- ( y e. C -> A e. B )
	ralxfr.2	|- ( x e. B -> E. y e. C x = A )
	ralxfr.3	|- ( x = A -> ( ph <-> ps ) )
Assertion	rexxfr	|- ( E. x e. B ph <-> E. y e. C ps )

Proof

Step	Hyp	Ref	Expression
1		ralxfr.1	|- ( y e. C -> A e. B )
2		ralxfr.2	|- ( x e. B -> E. y e. C x = A )
3		ralxfr.3	|- ( x = A -> ( ph <-> ps ) )
4		dfrex2	|- ( E. x e. B ph <-> -. A. x e. B -. ph )
5		dfrex2	|- ( E. y e. C ps <-> -. A. y e. C -. ps )
6	3	notbid	|- ( x = A -> ( -. ph <-> -. ps ) )
7	1 2 6	ralxfr	|- ( A. x e. B -. ph <-> A. y e. C -. ps )
8	5 7	xchbinxr	|- ( E. y e. C ps <-> -. A. x e. B -. ph )
9	4 8	bitr4i	|- ( E. x e. B ph <-> E. y e. C ps )