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

Theorem cbvexv 2037
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 5-Aug-1993.)
Hypothesis
Ref Expression
cbvalv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvexv  |-  ( E. x ph  <->  E. y ps )
Distinct variable groups:    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvexv
StepHypRef Expression
1 nfv 1626 . 2  |-  F/ y
ph
2 nfv 1626 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvex 2020 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177   E.wex 1547
This theorem is referenced by:  eujust  2240  euind  3064  reuind  3080  cbvopab2v  4223  bm1.3ii  4274  zfun  4642  reusv2lem2  4665  relop  4963  dmcoss  5075  fv3  5684  exfo  5826  ac6sfi  7287  brwdom2  7474  aceq1  7931  aceq0  7932  aceq3lem  7934  dfac4  7936  kmlem2  7964  kmlem13  7975  axdc4lem  8268  zfac  8273  zfcndun  8423  zfcndac  8427  sup2  9896  supmul  9908  climmo  12278  summo  12438  gsumval3eu  15440  elpt  17525  usgraedg4  21272  prodmo  25041  wfrlem1  25280  frrlem1  25305  bpolyval  25809  fdc  26140  ax10ext  27275  fnchoice  27368  bnj1185  28503
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  ax-12 1939
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551
  Copyright terms: Public domain W3C validator