Theorem nfeu1 2609

Description: Bound-variable hypothesis builder for uniqueness. See also nfeu1ALT 2610. (Contributed by NM, 9-Jul-1994.) (Revised by Mario Carneiro, 7-Oct-2016.)

Assertion

Ref	Expression
nfeu1	⊢ Ⅎ𝑥∃!𝑥𝜑

Proof of Theorem nfeu1

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		eu6 2594	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
2		nfa1 2153	. . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
3	2	nfex 2333	. 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
4	1, 3	nfxfr 1855	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ↔ wb 209  ∀wal 1537  ∃wex 1782  Ⅎwnf 1786  ∃!weu 2588

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-10 2143  ax-11 2159  ax-12 2176

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-ex 1783  df-nf 1787  df-mo 2558  df-eu 2589

This theorem is referenced by:  eupicka  2656  2eu8  2681  nfreu1  3286  eusv2i  5256  eusv2nf  5257  reusv2lem3  5262  iota2  6317  sniota  6319  fv3  6669  tz6.12c  6676  eusvobj1  7137  opiota  7754  dfac5lem5  9572  bnj1366  32314  bnj849  32410  pm14.24  41494  eu2ndop1stv  44034  tz6.12c-afv2  44151  setrec2lem2  45574