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

Theorem nfeu1 2508
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 2502 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 nfa1 2068 . . 3 𝑥𝑥(𝜑𝑥 = 𝑦)
32nfex 2192 . 2 𝑥𝑦𝑥(𝜑𝑥 = 𝑦)
41, 3nfxfr 1819 1 𝑥∃!𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1521  wex 1744  wnf 1748  ∃!weu 2498
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-10 2059  ax-11 2074  ax-12 2087
This theorem depends on definitions:  df-bi 197  df-or 384  df-ex 1745  df-nf 1750  df-eu 2502
This theorem is referenced by:  nfmo1  2509  eupicka  2566  2eu8  2589  exists2  2591  nfreu1  3139  eusv2i  4893  eusv2nf  4894  reusv2lem3  4901  iota2  5915  sniota  5916  fv3  6244  tz6.12c  6251  eusvobj1  6684  opiota  7273  dfac5lem5  8988  bnj1366  31026  bnj849  31121  pm14.24  38950  eu2ndop1stv  41523  setrec2lem2  42766
  Copyright terms: Public domain W3C validator