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  3380  eusv2i  5341  eusv2nf  5342  reusv2lem3  5347  iota2  6489  sniota  6491  fv3  6860  eusvobj1  7361  opiota  8013  dfac5lem5  10049  bnj1366  35005  bnj849  35101  pm14.24  44788  eu2ndop1stv  47485  tz6.12c-afv2  47602  setrec2lem2  50053