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	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
	reuxfr1dd.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
	reuxfr1dd.3	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	reuxfr1dd	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑦 ∈ 𝐶 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		reuxfr1dd.1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐶 ) → 𝐴 ∈ 𝐵 )
2		reuxfr1dd.2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
3		reuxfr1dd.3	⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) ) → ( 𝜓 ↔ 𝜒 ) )
4		reurex	⊢ ( ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 → ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
5	2 4	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
6	5	biantrurd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝜓 ↔ ( ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ∧ 𝜓 ) ) )
7		r19.41v	⊢ ( ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ( ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ∧ 𝜓 ) )
8	3	pm5.32da	⊢ ( 𝜑 → ( ( ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) ∧ 𝜓 ) ↔ ( ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) ∧ 𝜒 ) ) )
9		anass	⊢ ( ( ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) ∧ 𝜓 ) ↔ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) )
10		anass	⊢ ( ( ( 𝑦 ∈ 𝐶 ∧ 𝑥 = 𝐴 ) ∧ 𝜒 ) ↔ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜒 ) ) )
11	8 9 10	3bitr3g	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜓 ) ) ↔ ( 𝑦 ∈ 𝐶 ∧ ( 𝑥 = 𝐴 ∧ 𝜒 ) ) ) )
12	11	rexbidv2	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜒 ) ) )
13	7 12	bitr3id	⊢ ( 𝜑 → ( ( ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜒 ) ) )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( ( ∃ 𝑦 ∈ 𝐶 𝑥 = 𝐴 ∧ 𝜓 ) ↔ ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜒 ) ) )
15	6 14	bitrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ( 𝜓 ↔ ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜒 ) ) )
16	15	reubidva	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜒 ) ) )
17		reurmo	⊢ ( ∃! 𝑦 ∈ 𝐶 𝑥 = 𝐴 → ∃* 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
18	2 17	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐵 ) → ∃* 𝑦 ∈ 𝐶 𝑥 = 𝐴 )
19	1 18	reuxfrd	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 ∃ 𝑦 ∈ 𝐶 ( 𝑥 = 𝐴 ∧ 𝜒 ) ↔ ∃! 𝑦 ∈ 𝐶 𝜒 ) )
20	16 19	bitrd	⊢ ( 𝜑 → ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑦 ∈ 𝐶 𝜒 ) )