Metamath Proof Explorer


Theorem injust

Description: Soundness justification theorem for df-in . (Contributed by Rodolfo Medina, 28-Apr-2010) (Proof shortened by Andrew Salmon, 9-Jul-2011)

Ref Expression
Assertion injust { 𝑥 ∣ ( 𝑥𝐴𝑥𝐵 ) } = { 𝑦 ∣ ( 𝑦𝐴𝑦𝐵 ) }

Proof

Step Hyp Ref Expression
1 eleq1w ( 𝑥 = 𝑧 → ( 𝑥𝐴𝑧𝐴 ) )
2 eleq1w ( 𝑥 = 𝑧 → ( 𝑥𝐵𝑧𝐵 ) )
3 1 2 anbi12d ( 𝑥 = 𝑧 → ( ( 𝑥𝐴𝑥𝐵 ) ↔ ( 𝑧𝐴𝑧𝐵 ) ) )
4 3 cbvabv { 𝑥 ∣ ( 𝑥𝐴𝑥𝐵 ) } = { 𝑧 ∣ ( 𝑧𝐴𝑧𝐵 ) }
5 eleq1w ( 𝑧 = 𝑦 → ( 𝑧𝐴𝑦𝐴 ) )
6 eleq1w ( 𝑧 = 𝑦 → ( 𝑧𝐵𝑦𝐵 ) )
7 5 6 anbi12d ( 𝑧 = 𝑦 → ( ( 𝑧𝐴𝑧𝐵 ) ↔ ( 𝑦𝐴𝑦𝐵 ) ) )
8 7 cbvabv { 𝑧 ∣ ( 𝑧𝐴𝑧𝐵 ) } = { 𝑦 ∣ ( 𝑦𝐴𝑦𝐵 ) }
9 4 8 eqtri { 𝑥 ∣ ( 𝑥𝐴𝑥𝐵 ) } = { 𝑦 ∣ ( 𝑦𝐴𝑦𝐵 ) }