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

Theorem nfeu1 2631
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 2625 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 nfa1 2187 . . 3 𝑥𝑥(𝜑𝑥 = 𝑦)
32nfex 2321 . 2 𝑥𝑦𝑥(𝜑𝑥 = 𝑦)
41, 3nfxfr 1932 1 𝑥∃!𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 197  wal 1632  wex 1855  wnf 1859  ∃!weu 2621
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-10 2177  ax-11 2193  ax-12 2206
This theorem depends on definitions:  df-bi 198  df-or 864  df-ex 1856  df-nf 1861  df-eu 2625
This theorem is referenced by:  nfmo1  2632  eupicka  2689  2eu8  2712  exists2  2714  nfreu1  3262  eusv2i  5008  eusv2nf  5009  reusv2lem3  5014  iota2  6031  sniota  6032  fv3  6364  tz6.12c  6371  eusvobj1  6806  opiota  7399  dfac5lem5  9171  bnj1366  31255  bnj849  31350  pm14.24  39172  eu2ndop1stv  41747  setrec2lem2  42993
  Copyright terms: Public domain W3C validator