Theorem nfeu1 2623

Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT 2622 for a shorter proof using ax-12 2219. 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 1941 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 2603	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2		nfe1 2191	. . 3 ⊢ Ⅎ𝑥∃𝑥𝜑
3		nfmo1 2591	. . 3 ⊢ Ⅎ𝑥∃*𝑥𝜑
4	2, 3	nfan 1926	. 2 ⊢ Ⅎ𝑥(∃𝑥𝜑 ∧ ∃*𝑥𝜑)
5	1, 4	nfxfr 1880	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ∧ wa 400  ∃wex 1806  Ⅎwnf 1810  ∃*wmo 2571  ∃!weu 2602

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-10 2182  ax-11 2198

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-nf 1811  df-mo 2573  df-eu 2603

This theorem is referenced by:  eupicka  2668  2eu8  2692  nfreu1  3404  eusv2i  5366  eusv2nf  5367  reusv2lem3  5372  iota2  6526  sniota  6528  fv3  6900  eusvobj1  7404  opiota  8056  dfac5lem5  10111  bnj1366  35162  bnj849  35258  pm14.24  45034  eu2ndop1stv  47751  tz6.12c-afv2  47868  setrec2lem2  50357