Metamath Proof Explorer

Theorem nfrmod

Description: Deduction version of nfrmo . Usage of this theorem is discouraged because it depends on ax-13 . (Contributed by NM, 17-Jun-2017) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nfreud.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfreud.2 ${⊢}{\phi }\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
3 nfreud.3 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
4 df-rmo ${⊢}{\exists }^{*}{y}\in {A}{\psi }↔{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {\psi }\right)$
5 nfcvf ${⊢}¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
6 5 adantl ${⊢}\left({\phi }\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{y}$
7 2 adantr ${⊢}\left({\phi }\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to \underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}{A}$
8 6 7 nfeld ${⊢}\left({\phi }\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}\in {A}$
9 3 adantr ${⊢}\left({\phi }\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
10 8 9 nfand ${⊢}\left({\phi }\wedge ¬\forall {x}\phantom{\rule{.4em}{0ex}}{x}={y}\right)\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {\psi }\right)$
11 1 10 nfmod2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}\wedge {\psi }\right)$
12 4 11 nfxfrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\in {A}{\psi }$