Theorem cbveudavw

Description: Change bound variable in the existential uniqueness quantifier. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypothesis	cbveudavw.1	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	cbveudavw	⊢ ( 𝜑 → ( ∃! 𝑥 𝜓 ↔ ∃! 𝑦 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		cbveudavw.1	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) )
2	1	cbvexdvaw	⊢ ( 𝜑 → ( ∃ 𝑥 𝜓 ↔ ∃ 𝑦 𝜒 ) )
3	1	cbvmodavw	⊢ ( 𝜑 → ( ∃* 𝑥 𝜓 ↔ ∃* 𝑦 𝜒 ) )
4	2 3	anbi12d	⊢ ( 𝜑 → ( ( ∃ 𝑥 𝜓 ∧ ∃* 𝑥 𝜓 ) ↔ ( ∃ 𝑦 𝜒 ∧ ∃* 𝑦 𝜒 ) ) )
5		df-eu	⊢ ( ∃! 𝑥 𝜓 ↔ ( ∃ 𝑥 𝜓 ∧ ∃* 𝑥 𝜓 ) )
6		df-eu	⊢ ( ∃! 𝑦 𝜒 ↔ ( ∃ 𝑦 𝜒 ∧ ∃* 𝑦 𝜒 ) )
7	4 5 6	3bitr4g	⊢ ( 𝜑 → ( ∃! 𝑥 𝜓 ↔ ∃! 𝑦 𝜒 ) )