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

Proof

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