Theorem nfeu1 2615

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

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 2565  df-eu 2595

This theorem is used by:  eupicka  2660  2eu8  2684  nfreu1  3394  eusv2i  5356  eusv2nf  5357  reusv2lem3  5362  iota2  6527  sniota  6529  fv3  6903  eusvobj1  7413  opiota  8070  setrec2lem2  9976  dfac5lem5  10206  bnj1366  35459  bnj849  35555  pm14.24  45415  eu2ndop1stv  48194  tz6.12c-afv2  48311