Theorem iotajust

Description: Soundness justification theorem for df-iota . (Contributed by Andrew Salmon, 29-Jun-2011)

	Ref	Expression
Assertion	iotajust	⊢ ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } }

Proof

Step	Hyp	Ref	Expression
1		sneq	⊢ ( 𝑦 = 𝑤 → { 𝑦 } = { 𝑤 } )
2	1	eqeq2d	⊢ ( 𝑦 = 𝑤 → ( { 𝑥 ∣ 𝜑 } = { 𝑦 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑤 } ) )
3	2	cbvabv	⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } }
4		sneq	⊢ ( 𝑤 = 𝑧 → { 𝑤 } = { 𝑧 } )
5	4	eqeq2d	⊢ ( 𝑤 = 𝑧 → ( { 𝑥 ∣ 𝜑 } = { 𝑤 } ↔ { 𝑥 ∣ 𝜑 } = { 𝑧 } ) )
6	5	cbvabv	⊢ { 𝑤 ∣ { 𝑥 ∣ 𝜑 } = { 𝑤 } } = { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } }
7	3 6	eqtri	⊢ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } }
8	7	unieqi	⊢ ∪ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∪ { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } }