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

Theorem cbvexv 1971
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 1672 . 2  |-  F/ y
ph
2 nfv 1672 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvex 1969 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1589
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593
This theorem is referenced by:  eujust  2256  euind  3135  reuind  3151  cbvopab2v  4354  bm1.3ii  4404  reusv2lem2  4482  relop  4977  dmcoss  5086  fv3  5691  exfo  5849  zfun  6362  ac6sfi  7544  brwdom2  7776  aceq1  8275  aceq0  8276  aceq3lem  8278  dfac4  8280  kmlem2  8308  kmlem13  8319  axdc4lem  8612  zfac  8617  zfcndun  8769  zfcndac  8773  sup2  10273  supmul  10285  climmo  13018  summo  13177  gsumval3eu  16360  elpt  18986  usgraedg4  23127  prodmo  27295  wfrlem1  27570  frrlem1  27614  fdc  28482  axc11next  29502  fnchoice  29593  bnj1185  31486
  Copyright terms: Public domain W3C validator