Theorem rmoxfrd

Description: Transfer "at most one" restricted quantification from a variable x to another variable y contained in expression A . (Contributed by Thierry Arnoux, 7-Apr-2017) (Revised by Thierry Arnoux, 8-Oct-2017)

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

Proof

Step	Hyp	Ref	Expression
1		rmoxfrd.1	|- ( ( ph /\ y e. C ) -> A e. B )
2		rmoxfrd.2	|- ( ( ph /\ x e. B ) -> E! y e. C x = A )
3		rmoxfrd.3	|- ( ( ph /\ x = A ) -> ( ps <-> ch ) )
4		reurex	|- ( E! y e. C x = A -> E. y e. C x = A )
5	2 4	syl	|- ( ( ph /\ x e. B ) -> E. y e. C x = A )
6	1 5 3	rexxfrd	|- ( ph -> ( E. x e. B ps <-> E. y e. C ch ) )
7		df-rex	|- ( E. x e. B ps <-> E. x ( x e. B /\ ps ) )
8		df-rex	|- ( E. y e. C ch <-> E. y ( y e. C /\ ch ) )
9	6 7 8	3bitr3g	|- ( ph -> ( E. x ( x e. B /\ ps ) <-> E. y ( y e. C /\ ch ) ) )
10	1 2 3	reuxfr1d	|- ( ph -> ( E! x e. B ps <-> E! y e. C ch ) )
11		df-reu	|- ( E! x e. B ps <-> E! x ( x e. B /\ ps ) )
12		df-reu	|- ( E! y e. C ch <-> E! y ( y e. C /\ ch ) )
13	10 11 12	3bitr3g	|- ( ph -> ( E! x ( x e. B /\ ps ) <-> E! y ( y e. C /\ ch ) ) )
14	9 13	imbi12d	|- ( ph -> ( ( E. x ( x e. B /\ ps ) -> E! x ( x e. B /\ ps ) ) <-> ( E. y ( y e. C /\ ch ) -> E! y ( y e. C /\ ch ) ) ) )
15		moeu	|- ( E* x ( x e. B /\ ps ) <-> ( E. x ( x e. B /\ ps ) -> E! x ( x e. B /\ ps ) ) )
16		moeu	|- ( E* y ( y e. C /\ ch ) <-> ( E. y ( y e. C /\ ch ) -> E! y ( y e. C /\ ch ) ) )
17	14 15 16	3bitr4g	|- ( ph -> ( E* x ( x e. B /\ ps ) <-> E* y ( y e. C /\ ch ) ) )
18		df-rmo	|- ( E* x e. B ps <-> E* x ( x e. B /\ ps ) )
19		df-rmo	|- ( E* y e. C ch <-> E* y ( y e. C /\ ch ) )
20	17 18 19	3bitr4g	|- ( ph -> ( E* x e. B ps <-> E* y e. C ch ) )