# Metamath Proof Explorer

## Theorem wl-dfrexv

Description: Alternate definition of restricted universal quantification ( df-wl-rex ) when x and A are disjoint. (Contributed by Wolf Lammen, 25-May-2023)

Ref Expression
Assertion wl-dfrexv ${⊢}\exists {x}:{A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$

### Proof

Step Hyp Ref Expression
1 wl-dfralv ${⊢}\forall {x}:{A}\phantom{\rule{.4em}{0ex}}¬{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{\phi }\right)$
2 1 notbii ${⊢}¬\forall {x}:{A}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{\phi }\right)$
3 df-wl-rex ${⊢}\exists {x}:{A}\phantom{\rule{.4em}{0ex}}{\phi }↔¬\forall {x}:{A}\phantom{\rule{.4em}{0ex}}¬{\phi }$
4 exnalimn ${⊢}\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)↔¬\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to ¬{\phi }\right)$
5 2 3 4 3bitr4i ${⊢}\exists {x}:{A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$