Theorem nfeu1 2588

Description: Bound-variable hypothesis builder for uniqueness. See also nfeu1ALT 2589. (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 2574	. 2 ⊢ (∃!𝑥𝜑 ↔ ∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦))
2		nfa1 2150	. . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
3	2	nfex 2322	. 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
4	1, 3	nfxfr 1856	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

Syntax hints:   ↔ wb 205  ∀wal 1537  ∃wex 1783  Ⅎwnf 1787  ∃!weu 2568

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-10 2139  ax-11 2156  ax-12 2173

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-ex 1784  df-nf 1788  df-mo 2540  df-eu 2569

This theorem is referenced by:  eupicka  2636  2eu8  2660  nfreu1  3296  eusv2i  5312  eusv2nf  5313  reusv2lem3  5318  iota2  6407  sniota  6409  fv3  6774  tz6.12c  6781  eusvobj1  7249  opiota  7872  dfac5lem5  9814  bnj1366  32709  bnj849  32805  pm14.24  41939  eu2ndop1stv  44504  tz6.12c-afv2  44621  setrec2lem2  46286