# Metamath Proof Explorer

## Theorem nfeu1ALT

Description: Alternate proof of nfeu1 . This illustrates the systematic way of proving nonfreeness in a defined expression: consider the definiens as a tree whose nodes are its subformulas, and prove by tree-induction nonfreeness of each node, starting from the leaves (generally using nfv or nf* theorems for previously defined expressions) and up to the root. Here, the definiens is a conjunction of two previously defined expressions, which automatically yields the present proof. (Contributed by BJ, 2-Oct-2022) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nfeu1ALT ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }$

### Proof

Step Hyp Ref Expression
1 df-eu ${⊢}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }↔\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
2 nfe1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }$
3 nfmo1 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }$
4 2 3 nfan ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\phantom{\rule{.4em}{0ex}}{\phi }\wedge {\exists }^{*}{x}\phantom{\rule{.4em}{0ex}}{\phi }\right)$
5 1 4 nfxfr ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}\exists !{x}\phantom{\rule{.4em}{0ex}}{\phi }$