Theorem iotabi

Description: Equivalence theorem for descriptions. (Contributed by Andrew Salmon, 30-Jun-2011)

	Ref	Expression
Assertion	iotabi	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑥 𝜓 ) )

Proof

Step	Hyp	Ref	Expression
1		abbi1	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → { 𝑥 ∣ 𝜑 } = { 𝑥 ∣ 𝜓 } )
2	1	eqeq1d	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ { 𝑥 ∣ 𝜓 } = { 𝑧 } ) )
3	2	abbidv	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } } = { 𝑧 ∣ { 𝑥 ∣ 𝜓 } = { 𝑧 } } )
4	3	unieqd	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ∪ { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } } = ∪ { 𝑧 ∣ { 𝑥 ∣ 𝜓 } = { 𝑧 } } )
5		df-iota	⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } }
6		df-iota	⊢ ( ℩ 𝑥 𝜓 ) = ∪ { 𝑧 ∣ { 𝑥 ∣ 𝜓 } = { 𝑧 } }
7	4 5 6	3eqtr4g	⊢ ( ∀ 𝑥 ( 𝜑 ↔ 𝜓 ) → ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑥 𝜓 ) )