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

Theorem nfeu1 2590
Description: Bound-variable hypothesis builder for uniqueness. See also nfeu1ALT 2586. (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 2589 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 nfa1 2193 . . 3 𝑥𝑥(𝜑𝑥 = 𝑦)
32nfex 2327 . 2 𝑥𝑦𝑥(𝜑𝑥 = 𝑦)
41, 3nfxfr 1948 1 𝑥∃!𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 197  wal 1650  wex 1874  wnf 1878  ∃!weu 2581
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-10 2183  ax-11 2198  ax-12 2211
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-ex 1875  df-nf 1879  df-mo 2565  df-eu 2582
This theorem is referenced by:  nfmo1OLD  2612  eupicka  2659  2eu8  2682  exists2  2685  nfreu1  3257  eusv2i  5029  eusv2nf  5030  reusv2lem3  5035  iota2  6057  sniota  6058  fv3  6393  tz6.12c  6400  eusvobj1  6836  opiota  7429  dfac5lem5  9201  bnj1366  31348  bnj849  31443  pm14.24  39306  eu2ndop1stv  41873  tz6.12c-afv2  41990  setrec2lem2  43110
  Copyright terms: Public domain W3C validator