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

Theorem nfeu1 2608
 Description: Bound-variable hypothesis builder for uniqueness. See also nfeu1ALT 2609. (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 2593 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 nfa1 2152 . . 3 𝑥𝑥(𝜑𝑥 = 𝑦)
32nfex 2332 . 2 𝑥𝑦𝑥(𝜑𝑥 = 𝑦)
41, 3nfxfr 1854 1 𝑥∃!𝑥𝜑
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209  ∀wal 1536  ∃wex 1781  Ⅎwnf 1785  ∃!weu 2587 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 1911  ax-6 1970  ax-7 2015  ax-10 2142  ax-11 2158  ax-12 2175 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-ex 1782  df-nf 1786  df-mo 2557  df-eu 2588 This theorem is referenced by:  eupicka  2655  2eu8  2680  nfreu1  3288  eusv2i  5263  eusv2nf  5264  reusv2lem3  5269  iota2  6324  sniota  6326  fv3  6676  tz6.12c  6683  eusvobj1  7144  opiota  7761  dfac5lem5  9587  bnj1366  32329  bnj849  32425  pm14.24  41509  eu2ndop1stv  44049  tz6.12c-afv2  44166  setrec2lem2  45615
 Copyright terms: Public domain W3C validator