Theorem reuxfr1dd

Description: Transfer existential uniqueness from a variable x to another variable y contained in expression A . Simplifies reuxfr1d . (Contributed by Zhi Wang, 20-Sep-2025)

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

Proof

Step	Hyp	Ref	Expression
1		reuxfr1dd.1	|- ( ( ph /\ y e. C ) -> A e. B )
2		reuxfr1dd.2	|- ( ( ph /\ x e. B ) -> E! y e. C x = A )
3		reuxfr1dd.3	|- ( ( ph /\ ( y e. C /\ 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 -> ( ( ( y e. C /\ x = A ) /\ ps ) <-> ( ( y e. C /\ x = A ) /\ ch ) ) )
9		anass	|- ( ( ( y e. C /\ x = A ) /\ ps ) <-> ( y e. C /\ ( x = A /\ ps ) ) )
10		anass	|- ( ( ( y e. C /\ x = A ) /\ ch ) <-> ( y e. C /\ ( x = A /\ ch ) ) )
11	8 9 10	3bitr3g	|- ( ph -> ( ( y e. C /\ ( x = A /\ ps ) ) <-> ( y e. C /\ ( x = A /\ ch ) ) ) )
12	11	rexbidv2	|- ( ph -> ( E. y e. C ( x = A /\ ps ) <-> E. y e. C ( x = A /\ ch ) ) )
13	7 12	bitr3id	|- ( ph -> ( ( E. y e. C x = A /\ ps ) <-> E. y e. C ( x = A /\ ch ) ) )
14	13	adantr	|- ( ( ph /\ x e. B ) -> ( ( E. y e. C x = A /\ ps ) <-> E. y e. C ( x = A /\ ch ) ) )
15	6 14	bitrd	|- ( ( ph /\ x e. B ) -> ( ps <-> E. y e. C ( x = A /\ ch ) ) )
16	15	reubidva	|- ( ph -> ( E! x e. B ps <-> E! x e. B E. y e. C ( x = A /\ ch ) ) )
17		reurmo	|- ( E! y e. C x = A -> E* y e. C x = A )
18	2 17	syl	|- ( ( ph /\ x e. B ) -> E* y e. C x = A )
19	1 18	reuxfrd	|- ( ph -> ( E! x e. B E. y e. C ( x = A /\ ch ) <-> E! y e. C ch ) )
20	16 19	bitrd	|- ( ph -> ( E! x e. B ps <-> E! y e. C ch ) )