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

Theorem nfeu1 2166
 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 2160 . 2
2 nfa1 1768 . . 3
32nfex 1779 . 2
41, 3nfxfr 1560 1
 Colors of variables: wff set class Syntax hints:   wb 176  wal 1530  wex 1531  wnf 1534   wceq 1632  weu 2156 This theorem is referenced by:  nfmo1  2167  moaneu  2215  eupicka  2220  2eu8  2243  exists2  2246  nfreu1  2723  eusv2i  4547  eusv2nf  4548  reusv2lem3  4553  iota2  5261  sniota  5262  fv3  5557  tz6.12c  5563  opiota  6306  eusvobj1  6354  dfac5lem5  7770  pm14.24  27735  eu2ndop1stv  28083  bnj1366  29178  bnj849  29273 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727 This theorem depends on definitions:  df-bi 177  df-tru 1310  df-ex 1532  df-nf 1535  df-eu 2160
 Copyright terms: Public domain W3C validator