Theorem nfeu1

Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT for a shorter proof using ax-12 . This proof 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 the 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 NM, 9-Jul-1994) (Revised by Mario Carneiro, 7-Oct-2016) (Revised by BJ, 2-Oct-2022) (Proof modification is discouraged.)

	Ref	Expression
Assertion	nfeu1	$$⊢Ⅎx\exists !x\phi$$

Proof

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