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

Theorem nfeu1 2479
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 2473 . 2 (∃!𝑥𝜑 ↔ ∃𝑦𝑥(𝜑𝑥 = 𝑦))
2 nfa1 2025 . . 3 𝑥𝑥(𝜑𝑥 = 𝑦)
32nfex 2151 . 2 𝑥𝑦𝑥(𝜑𝑥 = 𝑦)
41, 3nfxfr 1776 1 𝑥∃!𝑥𝜑
Colors of variables: wff setvar class
Syntax hints:  wb 196  wal 1478  wex 1701  wnf 1705  ∃!weu 2469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-10 2016  ax-11 2031  ax-12 2044
This theorem depends on definitions:  df-bi 197  df-or 385  df-ex 1702  df-nf 1707  df-eu 2473
This theorem is referenced by:  nfmo1  2480  eupicka  2536  2eu8  2559  exists2  2561  nfreu1  3100  eusv2i  4823  eusv2nf  4824  reusv2lem3  4831  iota2  5836  sniota  5837  fv3  6163  tz6.12c  6170  eusvobj1  6598  opiota  7174  dfac5lem5  8894  bnj1366  30605  bnj849  30700  pm14.24  38112  eu2ndop1stv  40503  setrec2lem2  41731
  Copyright terms: Public domain W3C validator