Metamath Proof Explorer


Theorem rabeqi

Description: Equality theorem for restricted class abstractions. Inference form of rabeqf . (Contributed by Glauco Siliprandi, 26-Jun-2021) Avoid ax-10 and ax-11 . (Revised by Gino Giotto, 20-Aug-2023)

Ref Expression
Hypothesis rabeqi.1 A = B
Assertion rabeqi x A | φ = x B | φ

Proof

Step Hyp Ref Expression
1 rabeqi.1 A = B
2 1 nfth x A = B
3 eleq2 A = B x A x B
4 3 anbi1d A = B x A φ x B φ
5 2 4 abbid A = B x | x A φ = x | x B φ
6 df-rab x A | φ = x | x A φ
7 df-rab x B | φ = x | x B φ
8 5 6 7 3eqtr4g A = B x A | φ = x B | φ
9 1 8 ax-mp x A | φ = x B | φ