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

Theorem cbvexv 2053
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 2038 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  2256  euind  3081  reuind  3097  cbvopab2v  4242  bm1.3ii  4293  zfun  4661  reusv2lem2  4684  relop  4982  dmcoss  5094  fv3  5703  exfo  5846  ac6sfi  7310  brwdom2  7497  aceq1  7954  aceq0  7955  aceq3lem  7957  dfac4  7959  kmlem2  7987  kmlem13  7998  axdc4lem  8291  zfac  8296  zfcndun  8446  zfcndac  8450  sup2  9920  supmul  9932  climmo  12306  summo  12466  gsumval3eu  15468  elpt  17557  usgraedg4  21359  prodmo  25215  wfrlem1  25470  frrlem1  25495  bpolyval  25999  fdc  26339  ax10ext  27474  fnchoice  27567  bnj1185  28871
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946
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