Theorem reuxfr1d

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Cf. reuxfr1ds . (Contributed by Thierry Arnoux, 7-Apr-2017)

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

Proof

Step	Hyp	Ref	Expression
1		reuxfr1d.1	|- ( ( ph /\ y e. C ) -> A e. B )
2		reuxfr1d.2	|- ( ( ph /\ x e. B ) -> E! y e. C x = A )
3		reuxfr1d.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	5	biantrurd	|- ( ( ph /\ x e. B ) -> ( ps <-> ( E. y e. C x = A /\ ps ) ) )
7		r19.41v	|- ( E. y e. C ( x = A /\ ps ) <-> ( E. y e. C x = A /\ ps ) )
8	3	pm5.32da	|- ( ph -> ( ( x = A /\ ps ) <-> ( x = A /\ ch ) ) )
9	8	rexbidv	|- ( ph -> ( E. y e. C ( x = A /\ ps ) <-> E. y e. C ( x = A /\ ch ) ) )
10	7 9	bitr3id	|- ( ph -> ( ( E. y e. C x = A /\ ps ) <-> E. y e. C ( x = A /\ ch ) ) )
11	10	adantr	|- ( ( ph /\ x e. B ) -> ( ( E. y e. C x = A /\ ps ) <-> E. y e. C ( x = A /\ ch ) ) )
12	6 11	bitrd	|- ( ( ph /\ x e. B ) -> ( ps <-> E. y e. C ( x = A /\ ch ) ) )
13	12	reubidva	|- ( ph -> ( E! x e. B ps <-> E! x e. B E. y e. C ( x = A /\ ch ) ) )
14		reurmo	|- ( E! y e. C x = A -> E* y e. C x = A )
15	2 14	syl	|- ( ( ph /\ x e. B ) -> E* y e. C x = A )
16	1 15	reuxfrd	|- ( ph -> ( E! x e. B E. y e. C ( x = A /\ ch ) <-> E! y e. C ch ) )
17	13 16	bitrd	|- ( ph -> ( E! x e. B ps <-> E! y e. C ch ) )