MPE Home 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  |-  F/ x E! x ph

Proof of Theorem nfeu1
Dummy variable  y is distinct from all other variables.
StepHypRef Expression
1 df-eu 2160 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 nfa1 1768 . . 3  |-  F/ x A. x ( ph  <->  x  =  y )
32nfex 1779 . 2  |-  F/ x E. y A. x (
ph 
<->  x  =  y )
41, 3nfxfr 1560 1  |-  F/ x E! x ph
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1530   E.wex 1531   F/wnf 1534    = wceq 1632   E!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