Theorem nfeu1 2617

Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT 2616 for a shorter proof using ax-12 2215. 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 1948 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 2597	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2		nfe1 2189	. . 3 ⊢ Ⅎ𝑥∃𝑥𝜑
3		nfmo1 2585	. . 3 ⊢ Ⅎ𝑥∃*𝑥𝜑
4	2, 3	nfan 1933	. 2 ⊢ Ⅎ𝑥(∃𝑥𝜑 ∧ ∃*𝑥𝜑)
5	1, 4	nfxfr 1885	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1811  Ⅎwnf 1815  ∃*wmo 2565  ∃!weu 2596

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1944  ax-6 2001  ax-7 2042  ax-10 2179  ax-11 2196

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-nf 1816  df-mo 2567  df-eu 2597

This theorem is used by:  eupicka  2662  2eu8  2686  nfreu1  3396  eusv2i  5359  eusv2nf  5360  reusv2lem3  5365  iota2  6534  sniota  6537  fv3  6911  eusvobj1  7420  opiota  8078  setrec2lem2  9986  dfac5lem5  10216  bnj1366  35512  bnj849  35608  pm14.24  45555  eu2ndop1stv  48334  tz6.12c-afv2  48451