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

Theorem nfeu1 2296
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 2288 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 nfa1 1902 . . 3  |-  F/ x A. x ( ph  <->  x  =  y )
32nfex 1953 . 2  |-  F/ x E. y A. x (
ph 
<->  x  =  y )
41, 3nfxfr 1650 1  |-  F/ x E! x ph
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184   A.wal 1396   E.wex 1617   F/wnf 1621   E!weu 2284
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859
This theorem depends on definitions:  df-bi 185  df-ex 1618  df-nf 1622  df-eu 2288
This theorem is referenced by:  nfmo1  2297  eupicka  2356  2eu8  2383  exists2  2386  nfreu1  3025  eusv2i  4634  eusv2nf  4635  reusv2lem3  4640  iota2  5560  sniota  5561  fv3  5861  tz6.12c  5867  eusvobj1  6264  opiota  6832  dfac5lem5  8499  pm14.24  31583  eu2ndop1stv  32449  bnj1366  34308  bnj849  34403
  Copyright terms: Public domain W3C validator