This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iotaeq

Description: Equality theorem for descriptions. Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by Andrew Salmon, 30-Jun-2011) (New usage is discouraged.)

Ref Expression
Assertion iotaeq ( ∀ 𝑥 𝑥 = 𝑦 → ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 𝜑 ) )

Proof

Step Hyp Ref Expression
1 drsb1 ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( [ 𝑧 / 𝑥 ] 𝜑 ↔ [ 𝑧 / 𝑦 ] 𝜑 ) )
2 df-clab ⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ↔ [ 𝑧 / 𝑥 ] 𝜑 )
3 df-clab ⊢ ( 𝑧 ∈ { 𝑦 ∣ 𝜑 } ↔ [ 𝑧 / 𝑦 ] 𝜑 )
4 1 2 3 3bitr4g ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( 𝑧 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝑧 ∈ { 𝑦 ∣ 𝜑 } ) )
5 4 eqrdv ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → { 𝑥 ∣ 𝜑 } = { 𝑦 ∣ 𝜑 } )
6 5 eqeq1d ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( { 𝑥 ∣ 𝜑 } = { 𝑧 } ↔ { 𝑦 ∣ 𝜑 } = { 𝑧 } ) )
7 6 abbidv ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } } = { 𝑧 ∣ { 𝑦 ∣ 𝜑 } = { 𝑧 } } )
8 7 unieqd ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ∪ { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } } = ∪ { 𝑧 ∣ { 𝑦 ∣ 𝜑 } = { 𝑧 } } )
9 df-iota ⊢ ( ℩ 𝑥 𝜑 ) = ∪ { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } }
10 df-iota ⊢ ( ℩ 𝑦 𝜑 ) = ∪ { 𝑧 ∣ { 𝑦 ∣ 𝜑 } = { 𝑧 } }
11 8 9 10 3eqtr4g ⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 𝜑 ) )