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

Theorem cbvexv 1956
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 1609 . 2  |-  F/ y
ph
2 nfv 1609 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvex 1938 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176   E.wex 1531
This theorem is referenced by:  eujust  2158  euind  2965  reuind  2981  cbvopab2v  4109  bm1.3ii  4160  zfun  4529  reusv2lem2  4552  relop  4850  dmcoss  4960  fv3  5557  exfo  5694  ac6sfi  7117  brwdom2  7303  aceq1  7760  aceq0  7761  aceq3lem  7763  dfac4  7765  kmlem2  7793  kmlem13  7804  axdc4lem  8097  zfac  8102  zfcndun  8253  zfcndac  8257  sup2  9726  supmul  9738  climmo  12047  summo  12206  gsumval3eu  15206  elpt  17283  prodmo  24159  wfrlem1  24327  frrlem1  24352  bpolyval  24856  fdc  26558  ax10ext  27709  fnchoice  27803  bnj1185  29142
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535
  Copyright terms: Public domain W3C validator