# Metamath Proof Explorer

## Theorem ralnex

Description: Relationship between restricted universal and existential quantifiers. (Contributed by NM, 21-Jan-1997) (Proof shortened by BJ, 16-Jul-2021)

Ref Expression
Assertion ralnex ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 raln ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }↔\forall {x}\phantom{\rule{.4em}{0ex}}¬\left({x}\in {A}\wedge {\phi }\right)$
2 alnex ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\left({x}\in {A}\wedge {\phi }\right)↔¬\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
3 df-rex ${⊢}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }↔\exists {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\wedge {\phi }\right)$
4 2 3 xchbinxr ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}¬\left({x}\in {A}\wedge {\phi }\right)↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$
5 1 4 bitri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}¬{\phi }↔¬\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{\phi }$