Theorem nfeu1 2617

Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT 2616 for a shorter proof using ax-12 2213. 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 1944 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 2185	. . 3 ⊢ Ⅎ𝑥∃𝑥𝜑
3		nfmo1 2585	. . 3 ⊢ Ⅎ𝑥∃*𝑥𝜑
4	2, 3	nfan 1929	. 2 ⊢ Ⅎ𝑥(∃𝑥𝜑 ∧ ∃*𝑥𝜑)
5	1, 4	nfxfr 1883	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ∧ wa 400  ∃wex 1809  Ⅎwnf 1813  ∃*wmo 2565  ∃!weu 2596

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-10 2176  ax-11 2192

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-mo 2567  df-eu 2597

This theorem is referenced by:  eupicka  2662  2eu8  2686  nfreu1  3397  eusv2i  5365  eusv2nf  5366  reusv2lem3  5371  iota2  6525  sniota  6527  fv3  6899  eusvobj1  7403  opiota  8052  dfac5lem5  10107  bnj1366  35217  bnj849  35313  pm14.24  45162  eu2ndop1stv  47882  tz6.12c-afv2  47999  setrec2lem2  50492