Theorem nfeu1 2589

Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT 2588 for a shorter proof using ax-12 2185. 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 1916 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 2156	. . 3 ⊢ Ⅎ𝑥∃𝑥𝜑
3		nfmo1 2557	. . 3 ⊢ Ⅎ𝑥∃*𝑥𝜑
4	2, 3	nfan 1901	. 2 ⊢ Ⅎ𝑥(∃𝑥𝜑 ∧ ∃*𝑥𝜑)
5	1, 4	nfxfr 1855	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-10 2147  ax-11 2163

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-mo 2539  df-eu 2569

This theorem is referenced by:  eupicka  2634  2eu8  2659  nfreu1  3370  eusv2i  5336  eusv2nf  5337  reusv2lem3  5342  iota2  6487  sniota  6489  fv3  6858  eusvobj1  7360  opiota  8012  dfac5lem5  10049  bnj1366  34971  bnj849  35067  pm14.24  44859  eu2ndop1stv  47573  tz6.12c-afv2  47690  setrec2lem2  50169