Metamath Proof Explorer


Theorem rabeqbii

Description: Equality theorem for restricted class abstractions. Inference version. (Contributed by GG, 1-Sep-2025)

Ref Expression
Hypotheses rabeqbii.1 𝐴 = 𝐵
rabeqbii.2 ( 𝜑𝜓 )
Assertion rabeqbii { 𝑥𝐴𝜑 } = { 𝑥𝐵𝜓 }

Proof

Step Hyp Ref Expression
1 rabeqbii.1 𝐴 = 𝐵
2 rabeqbii.2 ( 𝜑𝜓 )
3 1 eleq2i ( 𝑥𝐴𝑥𝐵 )
4 3 2 anbi12i ( ( 𝑥𝐴𝜑 ) ↔ ( 𝑥𝐵𝜓 ) )
5 4 abbii { 𝑥 ∣ ( 𝑥𝐴𝜑 ) } = { 𝑥 ∣ ( 𝑥𝐵𝜓 ) }
6 df-rab { 𝑥𝐴𝜑 } = { 𝑥 ∣ ( 𝑥𝐴𝜑 ) }
7 df-rab { 𝑥𝐵𝜓 } = { 𝑥 ∣ ( 𝑥𝐵𝜓 ) }
8 5 6 7 3eqtr4i { 𝑥𝐴𝜑 } = { 𝑥𝐵𝜓 }