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

Theorem nfeu1 2329
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 2323 . 2  |-  ( E! x ph  <->  E. y A. x ( ph  <->  x  =  y ) )
2 nfa1 1999 . . 3  |-  F/ x A. x ( ph  <->  x  =  y )
32nfex 2050 . 2  |-  F/ x E. y A. x (
ph 
<->  x  =  y )
41, 3nfxfr 1704 1  |-  F/ x E! x ph
Colors of variables: wff setvar class
Syntax hints:    <-> wb 189   A.wal 1450   E.wex 1671   F/wnf 1675   E!weu 2319
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950
This theorem depends on definitions:  df-bi 190  df-ex 1672  df-nf 1676  df-eu 2323
This theorem is referenced by:  nfmo1  2330  eupicka  2386  2eu8  2409  exists2  2411  nfreu1  2947  eusv2i  4598  eusv2nf  4599  reusv2lem3  4604  iota2  5579  sniota  5580  fv3  5892  tz6.12c  5898  eusvobj1  6302  opiota  6871  dfac5lem5  8576  bnj1366  29713  bnj849  29808  pm14.24  36853  eu2ndop1stv  38768
  Copyright terms: Public domain W3C validator