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

Theorem nfeu1 2276
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 2269 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 nfa1 1952 . . 3  |-  F/ x A. x ( ph  <->  x  =  y )
32nfex 2004 . 2  |-  F/ x E. y A. x (
ph 
<->  x  =  y )
41, 3nfxfr 1692 1  |-  F/ x E! x ph
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187   A.wal 1435   E.wex 1659   F/wnf 1663   E!weu 2265
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905
This theorem depends on definitions:  df-bi 188  df-ex 1660  df-nf 1664  df-eu 2269
This theorem is referenced by:  nfmo1  2277  eupicka  2333  2eu8  2358  exists2  2360  nfreu1  2999  eusv2i  4618  eusv2nf  4619  reusv2lem3  4624  iota2  5588  sniota  5589  fv3  5891  tz6.12c  5897  eusvobj1  6296  opiota  6863  dfac5lem5  8559  bnj1366  29637  bnj849  29732  pm14.24  36641  eu2ndop1stv  38336
  Copyright terms: Public domain W3C validator