Theorem nfeu1 2589

Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT 2588 for a shorter proof using ax-12 2184. 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 1915 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.)

Assertion

Ref	Expression
nfeu1	⊢ Ⅎ𝑥∃!𝑥𝜑

Proof of Theorem nfeu1

Step	Hyp	Ref	Expression
1		df-eu 2569	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2		nfe1 2155	. . 3 ⊢ Ⅎ𝑥∃𝑥𝜑
3		nfmo1 2557	. . 3 ⊢ Ⅎ𝑥∃*𝑥𝜑
4	2, 3	nfan 1900	. 2 ⊢ Ⅎ𝑥(∃𝑥𝜑 ∧ ∃*𝑥𝜑)
5	1, 4	nfxfr 1854	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ∧ wa 395  ∃wex 1780  Ⅎwnf 1784  ∃*wmo 2537  ∃!weu 2568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-10 2146  ax-11 2162

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-mo 2539  df-eu 2569

This theorem is referenced by:  eupicka  2634  2eu8  2659  nfreu1  3378  eusv2i  5339  eusv2nf  5340  reusv2lem3  5345  iota2  6481  sniota  6483  fv3  6852  eusvobj1  7351  opiota  8003  dfac5lem5  10037  bnj1366  34985  bnj849  35081  pm14.24  44683  eu2ndop1stv  47381  tz6.12c-afv2  47498  setrec2lem2  49949