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	⊢ Ⅎ 𝑥 ∃! 𝑥 𝜑

Proof

Step	Hyp	Ref	Expression
1		df-eu	⊢ ( ∃! 𝑥 𝜑 ↔ ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 ) )
2		nfe1	⊢ Ⅎ 𝑥 ∃ 𝑥 𝜑
3		nfmo1	⊢ Ⅎ 𝑥 ∃* 𝑥 𝜑
4	2 3	nfan	⊢ Ⅎ 𝑥 ( ∃ 𝑥 𝜑 ∧ ∃* 𝑥 𝜑 )
5	1 4	nfxfr	⊢ Ⅎ 𝑥 ∃! 𝑥 𝜑