Theorem nfeu1 2590

Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT 2589 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 2570	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2		nfe1 2156	. . 3 ⊢ Ⅎ𝑥∃𝑥𝜑
3		nfmo1 2558	. . 3 ⊢ Ⅎ𝑥∃*𝑥𝜑
4	2, 3	nfan 1901	. 2 ⊢ Ⅎ𝑥(∃𝑥𝜑 ∧ ∃*𝑥𝜑)
5	1, 4	nfxfr 1855	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

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

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 2540  df-eu 2570

This theorem is referenced by:  eupicka  2635  2eu8  2660  nfreu1  3371  eusv2i  5332  eusv2nf  5333  reusv2lem3  5338  iota2  6482  sniota  6484  fv3  6853  eusvobj1  7354  opiota  8006  dfac5lem5  10043  bnj1366  34990  bnj849  35086  pm14.24  44880  eu2ndop1stv  47588  tz6.12c-afv2  47705  setrec2lem2  50184