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

Metamath Proof Explorer

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

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