# Metamath Proof Explorer

## Theorem rabbida

Description: Equivalent wff's yield equal restricted class abstractions (deduction form). Version of rabbidva with disjoint variable condition replaced by nonfreeness hypothesis. (Contributed by BJ, 27-Apr-2019)

Ref Expression
Hypotheses rabbida.n ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
rabbida.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({\psi }↔{\chi }\right)$
Assertion rabbida ${⊢}{\phi }\to \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}\in {A}|{\chi }\right\}$

### Proof

Step Hyp Ref Expression
1 rabbida.n ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\phi }$
2 rabbida.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({\psi }↔{\chi }\right)$
3 2 ex ${⊢}{\phi }\to \left({x}\in {A}\to \left({\psi }↔{\chi }\right)\right)$
4 1 3 ralrimi ${⊢}{\phi }\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }↔{\chi }\right)$
5 rabbi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({\psi }↔{\chi }\right)↔\left\{{x}\in {A}|{\psi }\right\}=\left\{{x}\in {A}|{\chi }\right\}$
6 4 5 sylib ${⊢}{\phi }\to \left\{{x}\in {A}|{\psi }\right\}=\left\{{x}\in {A}|{\chi }\right\}$