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

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.
StepHypRef Expression
1 eu6 2574 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 nfa1 2151 . . 3 𝑥𝑥(𝜑𝑥 = 𝑦)
32nfex 2324 . 2 𝑥𝑦𝑥(𝜑𝑥 = 𝑦)
41, 3nfxfr 1853 1 𝑥∃!𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 206  wal 1538  wex 1779  wnf 1783  ∃!weu 2568
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-10 2141  ax-11 2157  ax-12 2177
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-ex 1780  df-nf 1784  df-mo 2540  df-eu 2569
This theorem is referenced by:  eupicka  2634  2eu8  2659  nfreu1  3412  eusv2i  5394  eusv2nf  5395  reusv2lem3  5400  iota2  6550  sniota  6552  fv3  6924  tz6.12cOLD  6933  eusvobj1  7424  opiota  8084  dfac5lem5  10167  bnj1366  34843  bnj849  34939  pm14.24  44451  eu2ndop1stv  47137  tz6.12c-afv2  47254  setrec2lem2  49213
  Copyright terms: Public domain W3C validator