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

Theorem nfeu1 2153
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 2147 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 nfa1 1756 . . 3  |-  F/ x A. x ( ph  <->  x  =  y )
32nfex 1767 . 2  |-  F/ x E. y A. x (
ph 
<->  x  =  y )
41, 3nfxfr 1557 1  |-  F/ x E! x ph
Colors of variables: wff set class
Syntax hints:    <-> wb 176   A.wal 1527   E.wex 1528   F/wnf 1531    = wceq 1623   E!weu 2143
This theorem is referenced by:  nfmo1  2154  moaneu  2202  eupicka  2207  2eu8  2230  exists2  2233  nfreu1  2710  eusv2i  4531  eusv2nf  4532  reusv2lem3  4537  iota2  5245  sniota  5246  fv3  5541  tz6.12c  5547  opiota  6290  eusvobj1  6338  dfac5lem5  7754  pm14.24  27632  bnj1366  28862  bnj849  28957
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715
This theorem depends on definitions:  df-bi 177  df-tru 1310  df-ex 1529  df-nf 1532  df-eu 2147
  Copyright terms: Public domain W3C validator