# Metamath Proof Explorer

## Theorem nfraldw

Description: Deduction version of nfralw . Version of nfrald with a disjoint variable condition, which does not require ax-13 . (Contributed by NM, 15-Feb-2013) (Revised by Gino Giotto, 10-Jan-2024)

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

### Proof

Step Hyp Ref Expression
1 nfraldw.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfraldw.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 nfraldw.3 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
4 df-ral ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\psi }\right)$
5 nfcvd ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
6 5 2 nfeld ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
7 6 3 nfimd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\psi }\right)$
8 1 7 nfald ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\to {\psi }\right)$
9 4 8 nfxfrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{\psi }$