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 2148	. . 3 ⊢ Ⅎ𝑥∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
3	2	nfex 2318	. 2 ⊢ Ⅎ𝑥∃𝑦∀𝑥(𝜑 ↔ 𝑥 = 𝑦)
4	1, 3	nfxfr 1855	1 ⊢ Ⅎ𝑥∃!𝑥𝜑

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

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 1913  ax-6 1971  ax-7 2011  ax-10 2137  ax-11 2154  ax-12 2171

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-ex 1783  df-nf 1787  df-mo 2540  df-eu 2569

This theorem is referenced by:  eupicka  2636  2eu8  2660  nfreu1  3300  eusv2i  5317  eusv2nf  5318  reusv2lem3  5323  iota2  6422  sniota  6424  fv3  6792  tz6.12c  6799  eusvobj1  7269  opiota  7899  dfac5lem5  9883  bnj1366  32809  bnj849  32905  pm14.24  42050  eu2ndop1stv  44617  tz6.12c-afv2  44734  setrec2lem2  46400