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

Theorem nfeu1 2667
Description: Bound-variable hypothesis builder for uniqueness. See also nfeu1ALT 2668. (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 2652 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 nfa1 2146 . . 3 𝑥𝑥(𝜑𝑥 = 𝑦)
32nfex 2334 . 2 𝑥𝑦𝑥(𝜑𝑥 = 𝑦)
41, 3nfxfr 1844 1 𝑥∃!𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 207  wal 1526  wex 1771  wnf 1775  ∃!weu 2646
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-10 2136  ax-11 2151  ax-12 2167
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-ex 1772  df-nf 1776  df-mo 2615  df-eu 2647
This theorem is referenced by:  eupicka  2712  2eu8  2739  nfreu1  3368  eusv2i  5285  eusv2nf  5286  reusv2lem3  5291  iota2  6337  sniota  6339  fv3  6681  tz6.12c  6688  eusvobj1  7139  opiota  7746  dfac5lem5  9541  bnj1366  32000  bnj849  32096  pm14.24  40641  eu2ndop1stv  43201  tz6.12c-afv2  43318  setrec2lem2  44725
  Copyright terms: Public domain W3C validator