# Metamath Proof Explorer

## Theorem nfexd2

Description: Variation on nfexd which adds the hypothesis that x and y are distinct in the inner subproof. Usage of this theorem is discouraged because it depends on ax-13 . Check out nfexd for a version requiring fewer axioms. (Contributed by Mario Carneiro, 8-Oct-2016) (New usage is discouraged.)

Ref Expression
Hypotheses nfald2.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
nfald2.2 ${⊢}\left({\phi }\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
Assertion nfexd2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 nfald2.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfald2.2 ${⊢}\left({\phi }\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 df-ex ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }↔¬\forall {y}\phantom{\rule{.4em}{0ex}}¬{\psi }$
4 2 nfnd ${⊢}\left({\phi }\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬{\psi }$
5 1 4 nfald2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}¬{\psi }$
6 5 nfnd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}¬\forall {y}\phantom{\rule{.4em}{0ex}}¬{\psi }$
7 3 6 nfxfrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {y}\phantom{\rule{.4em}{0ex}}{\psi }$