# Metamath Proof Explorer

## Theorem rabeq0

Description: Condition for a restricted class abstraction to be empty. (Contributed by Jeff Madsen, 7-Jun-2010) (Revised by BJ, 16-Jul-2021)

Ref Expression
Assertion rabeq0 ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\varnothing ↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }$

### Proof

Step Hyp Ref Expression
1 ab0 ${⊢}\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}=\varnothing ↔\forall {x}\phantom{\rule{.4em}{0ex}}¬\left({x}\in {A}\wedge {\phi }\right)$
2 df-rab ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}$
3 2 eqeq1i ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\varnothing ↔\left\{{x}|\left({x}\in {A}\wedge {\phi }\right)\right\}=\varnothing$
4 raln ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}¬\left({x}\in {A}\wedge {\phi }\right)$
5 1 3 4 3bitr4i ${⊢}\left\{{x}\in {A}|{\phi }\right\}=\varnothing ↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }$