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\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$$