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	⊢ ( ∀ 𝑥 𝑥 = 𝑦 → ( ℩ 𝑥 𝜑 ) = ( ℩ 𝑦 𝜑 ) )