Metamath Proof Explorer


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