Theorem moxfr

Description: Transfer at-most-one between related expressions. (Contributed by Stefan O'Rear, 12-Feb-2015)

	Ref	Expression
Hypotheses	moxfr.a	|- A e. _V
	moxfr.b	|- E! y x = A
	moxfr.c	|- ( x = A -> ( ph <-> ps ) )
Assertion	moxfr	|- ( E* x ph <-> E* y ps )

Proof

Step	Hyp	Ref	Expression
1		moxfr.a	|- A e. _V
2		moxfr.b	|- E! y x = A
3		moxfr.c	|- ( x = A -> ( ph <-> ps ) )
4	1	a1i	|- ( y e. _V -> A e. _V )
5		euex	|- ( E! y x = A -> E. y x = A )
6	2 5	ax-mp	|- E. y x = A
7		rexv	|- ( E. y e. _V x = A <-> E. y x = A )
8	6 7	mpbir	|- E. y e. _V x = A
9	8	a1i	|- ( x e. _V -> E. y e. _V x = A )
10	4 9 3	rexxfr	|- ( E. x e. _V ph <-> E. y e. _V ps )
11		rexv	|- ( E. x e. _V ph <-> E. x ph )
12		rexv	|- ( E. y e. _V ps <-> E. y ps )
13	10 11 12	3bitr3i	|- ( E. x ph <-> E. y ps )
14	1 2 3	euxfrw	|- ( E! x ph <-> E! y ps )
15	13 14	imbi12i	|- ( ( E. x ph -> E! x ph ) <-> ( E. y ps -> E! y ps ) )
16		moeu	|- ( E* x ph <-> ( E. x ph -> E! x ph ) )
17		moeu	|- ( E* y ps <-> ( E. y ps -> E! y ps ) )
18	15 16 17	3bitr4i	|- ( E* x ph <-> E* y ps )