Theorem nfeu1 2581

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

Syntax hints:   ↔ wb 205  ∀wal 1539  ∃wex 1781  Ⅎwnf 1785  ∃!weu 2561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 846  df-ex 1782  df-nf 1786  df-mo 2533  df-eu 2562

This theorem is referenced by:  eupicka  2629  2eu8  2653  nfreu1  3407  eusv2i  5385  eusv2nf  5386  reusv2lem3  5391  iota2  6521  sniota  6523  fv3  6896  tz6.12cOLD  6905  eusvobj1  7386  opiota  8027  dfac5lem5  10104  bnj1366  33669  bnj849  33765  pm14.24  42960  eu2ndop1stv  45603  tz6.12c-afv2  45720  setrec2lem2  47385