# Metamath Proof Explorer

## Theorem nfmodv

Description: Bound-variable hypothesis builder for the at-most-one quantifier. See nfmod for a version without disjoint variable conditions but requiring ax-13 . (Contributed by Mario Carneiro, 14-Nov-2016) (Revised by BJ, 28-Jan-2023)

Ref Expression
Hypotheses nfmodv.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
nfmodv.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
Assertion nfmodv ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{\psi }$

### Proof

Step Hyp Ref Expression
1 nfmodv.1 ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{\phi }$
2 nfmodv.2 ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\psi }$
3 df-mo ${⊢}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{\psi }↔\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {y}={z}\right)$
4 nfv ${⊢}Ⅎ{z}\phantom{\rule{.4em}{0ex}}{\phi }$
5 nfvd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{y}={z}$
6 2 5 nfimd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {y}={z}\right)$
7 1 6 nfald ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {y}={z}\right)$
8 4 7 nfexd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({\psi }\to {y}={z}\right)$
9 3 8 nfxfrd ${⊢}{\phi }\to Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{y}\phantom{\rule{.4em}{0ex}}{\psi }$