# Metamath Proof Explorer

## Theorem rabeqf

Description: Equality theorem for restricted class abstractions, with bound-variable hypotheses instead of distinct variable restrictions. (Contributed by NM, 7-Mar-2004)

Ref Expression
Hypotheses rabeqf.1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
rabeqf.2 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{B}$
Assertion rabeqf ${⊢}{A}={B}\to \left\{{x}\in {A}|{\phi }\right\}=\left\{{x}\in {B}|{\phi }\right\}$

### Proof

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