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

Theorem nfeu1 2609
 Description: Bound-variable hypothesis builder for uniqueness. (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 df-eu 2603 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 nfa1 2169 . . 3 𝑥𝑥(𝜑𝑥 = 𝑦)
32nfex 2293 . 2 𝑥𝑦𝑥(𝜑𝑥 = 𝑦)
41, 3nfxfr 1920 1 𝑥∃!𝑥𝜑
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 196  ∀wal 1622  ∃wex 1845  Ⅎwnf 1849  ∃!weu 2599 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1863  ax-4 1878  ax-5 1980  ax-6 2046  ax-7 2082  ax-10 2160  ax-11 2175  ax-12 2188 This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1846  df-nf 1851  df-eu 2603 This theorem is referenced by:  nfmo1  2610  eupicka  2667  2eu8  2690  exists2  2692  nfreu1  3240  eusv2i  5004  eusv2nf  5005  reusv2lem3  5012  iota2  6030  sniota  6031  fv3  6359  tz6.12c  6366  eusvobj1  6799  opiota  7388  dfac5lem5  9132  bnj1366  31199  bnj849  31294  pm14.24  39127  eu2ndop1stv  41700  setrec2lem2  42943
 Copyright terms: Public domain W3C validator