Theorem aiotajust

Description: Soundness justification theorem for df-aiota . (Contributed by AV, 24-Aug-2022)

	Ref	Expression
Assertion	aiotajust	⊢ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∩ { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } }

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	inteqi	⊢ ∩ { 𝑦 ∣ { 𝑥 ∣ 𝜑 } = { 𝑦 } } = ∩ { 𝑧 ∣ { 𝑥 ∣ 𝜑 } = { 𝑧 } }