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

Theorem nfeu1 2294
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 2286 . 2
2 nfa1 1897 . . 3
32nfex 1948 . 2
41, 3nfxfr 1645 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  A.wal 1393  E.wex 1612  F/wnf 1616  E!weu 2282
This theorem is referenced by:  nfmo1  2295  eupicka  2359  2eu8  2386  exists2  2389  nfreu1  3028  eusv2i  4649  eusv2nf  4650  reusv2lem3  4655  iota2  5582  sniota  5583  fv3  5884  tz6.12c  5890  eusvobj1  6290  opiota  6859  dfac5lem5  8529  pm14.24  31339  eu2ndop1stv  32207  bnj1366  33888  bnj849  33983
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854
This theorem depends on definitions:  df-bi 185  df-ex 1613  df-nf 1617  df-eu 2286
  Copyright terms: Public domain W3C validator