Theorem nfeu1 2616

Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT 2615 for a shorter proof using ax-12 2212. 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 1934 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 2596	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2		nfe1 2184	. . 3 ⊢ Ⅎ𝑥∃𝑥𝜑
3		nfmo1 2584	. . 3 ⊢ Ⅎ𝑥∃*𝑥𝜑
4	2, 3	nfan 1919	. 2 ⊢ Ⅎ𝑥(∃𝑥𝜑 ∧ ∃*𝑥𝜑)
5	1, 4	nfxfr 1873	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ∧ wa 399  ∃wex 1799  Ⅎwnf 1803  ∃*wmo 2564  ∃!weu 2595

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-10 2175  ax-11 2191

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-ex 1800  df-nf 1804  df-mo 2566  df-eu 2596

This theorem is referenced by:  eupicka  2661  2eu8  2685  nfreu1  3395  eusv2i  5351  eusv2nf  5352  reusv2lem3  5357  iota2  6510  sniota  6512  fv3  6885  eusvobj1  7389  opiota  8040  dfac5lem5  10083  bnj1366  35124  bnj849  35220  pm14.24  45008  eu2ndop1stv  47719  tz6.12c-afv2  47836  setrec2lem2  50315