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

Theorem nfeu1 2248
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 2242 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 nfa1 1796 . . 3  |-  F/ x A. x ( ph  <->  x  =  y )
32nfex 1855 . 2  |-  F/ x E. y A. x (
ph 
<->  x  =  y )
41, 3nfxfr 1576 1  |-  F/ x E! x ph
Colors of variables: wff set class
Syntax hints:    <-> wb 177   A.wal 1546   E.wex 1547   F/wnf 1550   E!weu 2238
This theorem is referenced by:  nfmo1  2249  moaneu  2297  eupicka  2302  2eu8  2325  exists2  2328  nfreu1  2821  eusv2i  4660  eusv2nf  4661  reusv2lem3  4666  iota2  5384  sniota  5385  fv3  5684  tz6.12c  5690  opiota  6471  eusvobj1  6519  dfac5lem5  7941  pm14.24  27301  eu2ndop1stv  27648  bnj1366  28539  bnj849  28634
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-nf 1551  df-eu 2242
  Copyright terms: Public domain W3C validator