# Metamath Proof Explorer

## Theorem nfrexd

Description: Deduction version of nfrex . (Contributed by Mario Carneiro, 14-Oct-2016) Add disjoint variable condition to avoid ax-13 . See nfrexdg for a less restrictive version requiring more axioms. (Revised by Gino Giotto, 20-Jan-2024)

Ref Expression
Hypotheses nfrexd.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
nfrexd.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
nfrexd.3 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
Assertion nfrexd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 nfrexd.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfrexd.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 nfrexd.3 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
4 dfrex2 ${⊢}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{\psi }$
5 3 nfnd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
6 1 2 5 nfraldw ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{\psi }$
7 6 nfnd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}¬{\psi }$
8 4 7 nfxfrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$