Theorem nfeu1 2593

Description: Bound-variable hypothesis builder for uniqueness. See nfeu1ALT 2592 for a shorter proof using ax-12 2189. 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 1921 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 2573	. 2 ⊢ (∃!𝑥𝜑 ↔ (∃𝑥𝜑 ∧ ∃*𝑥𝜑))
2		nfe1 2161	. . 3 ⊢ Ⅎ𝑥∃𝑥𝜑
3		nfmo1 2561	. . 3 ⊢ Ⅎ𝑥∃*𝑥𝜑
4	2, 3	nfan 1906	. 2 ⊢ Ⅎ𝑥(∃𝑥𝜑 ∧ ∃*𝑥𝜑)
5	1, 4	nfxfr 1860	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ∧ wa 396  ∃wex 1786  Ⅎwnf 1790  ∃*wmo 2541  ∃!weu 2572

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-10 2152  ax-11 2168

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-nf 1791  df-mo 2543  df-eu 2573

This theorem is referenced by:  eupicka  2638  2eu8  2662  nfreu1  3372  eusv2i  5323  eusv2nf  5324  reusv2lem3  5329  iota2  6474  sniota  6476  fv3  6845  eusvobj1  7349  opiota  8001  dfac5lem5  10040  bnj1366  35011  bnj849  35107  pm14.24  44876  eu2ndop1stv  47588  tz6.12c-afv2  47705  setrec2lem2  50184