MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfeu1 Structured version   Visualization version   GIF version

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.
StepHypRef Expression
1 eu6 2567 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 nfa1 2148 . . 3 𝑥𝑥(𝜑𝑥 = 𝑦)
32nfex 2317 . 2 𝑥𝑦𝑥(𝜑𝑥 = 𝑦)
41, 3nfxfr 1855 1 𝑥∃!𝑥𝜑
Colors of variables: wff setvar class
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
  Copyright terms: Public domain W3C validator