Theorem nfeu1 2619

Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT 2618 for a shorter proof using ax-12 2216. 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 1947 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 2599	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2		nfe1 2188	. . 3 ⊢ Ⅎ𝑥∃𝑥𝜑
3		nfmo1 2587	. . 3 ⊢ Ⅎ𝑥∃*𝑥𝜑
4	2, 3	nfan 1932	. 2 ⊢ Ⅎ𝑥(∃𝑥𝜑 ∧ ∃*𝑥𝜑)
5	1, 4	nfxfr 1886	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

This proof depends on syntax axioms:   ∧ wa 401  ∃wex 1812  Ⅎwnf 1816  ∃*wmo 2567  ∃!weu 2598

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-10 2179  ax-11 2195

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-nf 1817  df-mo 2569  df-eu 2599

This theorem is used by:  eupicka  2664  2eu8  2688  nfreu1  3399  eusv2i  5367  eusv2nf  5368  reusv2lem3  5373  iota2  6529  sniota  6531  fv3  6903  eusvobj1  7412  opiota  8062  dfac5lem5  10127  bnj1366  35284  bnj849  35380  pm14.24  45202  eu2ndop1stv  47922  tz6.12c-afv2  48039  setrec2lem2  50531