Theorem nfeu1 2614

Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT 2613 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 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 2594	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2		nfe1 2187	. . 3 ⊢ Ⅎ𝑥∃𝑥𝜑
3		nfmo1 2582	. . 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 2562  ∃!weu 2593

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 2178  ax-11 2194

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 2564  df-eu 2594

This theorem is used by:  eupicka  2659  2eu8  2683  nfreu1  3393  eusv2i  5359  eusv2nf  5360  reusv2lem3  5365  iota2  6522  sniota  6524  fv3  6897  eusvobj1  7407  opiota  8057  dfac5lem5  10133  bnj1366  35341  bnj849  35437  pm14.24  45259  eu2ndop1stv  48016  tz6.12c-afv2  48133  setrec2lem2  50623