Theorem cbviotadavw

Description: Change bound variable in a description binder. Deduction form. (Contributed by GG, 14-Aug-2025)

	Ref	Expression
Hypothesis	cbviotadavw.1	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) )
Assertion	cbviotadavw	⊢ ( 𝜑 → ( ℩ 𝑥 𝜓 ) = ( ℩ 𝑦 𝜒 ) )

Proof

Step	Hyp	Ref	Expression
1		cbviotadavw.1	⊢ ( ( 𝜑 ∧ 𝑥 = 𝑦 ) → ( 𝜓 ↔ 𝜒 ) )
2	1	cbvabdavw	⊢ ( 𝜑 → { 𝑥 ∣ 𝜓 } = { 𝑦 ∣ 𝜒 } )
3	2	eqeq1d	⊢ ( 𝜑 → ( { 𝑥 ∣ 𝜓 } = { 𝑡 } ↔ { 𝑦 ∣ 𝜒 } = { 𝑡 } ) )
4	3	abbidv	⊢ ( 𝜑 → { 𝑡 ∣ { 𝑥 ∣ 𝜓 } = { 𝑡 } } = { 𝑡 ∣ { 𝑦 ∣ 𝜒 } = { 𝑡 } } )
5	4	unieqd	⊢ ( 𝜑 → ∪ { 𝑡 ∣ { 𝑥 ∣ 𝜓 } = { 𝑡 } } = ∪ { 𝑡 ∣ { 𝑦 ∣ 𝜒 } = { 𝑡 } } )
6		df-iota	⊢ ( ℩ 𝑥 𝜓 ) = ∪ { 𝑡 ∣ { 𝑥 ∣ 𝜓 } = { 𝑡 } }
7		df-iota	⊢ ( ℩ 𝑦 𝜒 ) = ∪ { 𝑡 ∣ { 𝑦 ∣ 𝜒 } = { 𝑡 } }
8	5 6 7	3eqtr4g	⊢ ( 𝜑 → ( ℩ 𝑥 𝜓 ) = ( ℩ 𝑦 𝜒 ) )