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 ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}\in {B}|{\phi }\right\}$

Proof

Step Hyp Ref Expression
1 rabeqi.1 ${⊢}{A}={B}$
2 1 nfth ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{A}={B}$
3 eleq2 ${⊢}{A}={B}\to \left({x}\in {A}↔{x}\in {B}\right)$
4 3 anbi1d ${⊢}{A}={B}\to \left(\left({x}\in {A}\wedge {\phi }\right)↔\left({x}\in {B}\wedge {\phi }\right)\right)$
5 2 4 abbid ${⊢}{A}={B}\to \left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}=\left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}$
6 df-rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
7 df-rab ${⊢}\left\{{x}\in {B}|{\phi }\right\}=\left\{{x}|\left({x}\in {B}\wedge {\phi }\right)\right\}$
8 5 6 7 3eqtr4g ${⊢}{A}={B}\to \left\{{x}\in {A}|{\phi }\right\}=\left\{{x}\in {B}|{\phi }\right\}$
9 1 8 ax-mp ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}\in {B}|{\phi }\right\}$