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

Theorem nfeu1 2288
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 2279 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 nfa1 1845 . . 3  |-  F/ x A. x ( ph  <->  x  =  y )
32nfex 1895 . 2  |-  F/ x E. y A. x (
ph 
<->  x  =  y )
41, 3nfxfr 1625 1  |-  F/ x E! x ph
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1377   E.wex 1596   F/wnf 1599   E!weu 2275
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803
This theorem depends on definitions:  df-bi 185  df-ex 1597  df-nf 1600  df-eu 2279
This theorem is referenced by:  nfmo1  2289  moaneuOLD  2359  eupicka  2365  2eu8  2396  exists2  2399  nfreu1  3032  eusv2i  4644  eusv2nf  4645  reusv2lem3  4650  iota2  5575  sniota  5576  fv3  5877  tz6.12c  5883  eusvobj1  6276  opiota  6840  dfac5lem5  8504  pm14.24  30917  eu2ndop1stv  31674  bnj1366  32967  bnj849  33062
  Copyright terms: Public domain W3C validator