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

Theorem nfeu1 2586
Description: Bound-variable hypothesis builder for uniqueness. See also nfeu1ALT 2587. (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 2572 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 nfa1 2149 . . 3 𝑥𝑥(𝜑𝑥 = 𝑦)
32nfex 2323 . 2 𝑥𝑦𝑥(𝜑𝑥 = 𝑦)
41, 3nfxfr 1850 1 𝑥∃!𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 206  wal 1535  wex 1776  wnf 1780  ∃!weu 2566
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-10 2139  ax-11 2155  ax-12 2175
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-ex 1777  df-nf 1781  df-mo 2538  df-eu 2567
This theorem is referenced by:  eupicka  2632  2eu8  2657  nfreu1  3410  eusv2i  5400  eusv2nf  5401  reusv2lem3  5406  iota2  6552  sniota  6554  fv3  6925  tz6.12cOLD  6934  eusvobj1  7424  opiota  8083  dfac5lem5  10165  bnj1366  34822  bnj849  34918  pm14.24  44428  eu2ndop1stv  47075  tz6.12c-afv2  47192  setrec2lem2  48925
  Copyright terms: Public domain W3C validator