This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \exists! x φ$

Proof

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