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

Theorem cbvexv 1972
Description: Rule used to change bound variables, using implicit substitution. (Contributed by NM, 21-Jun-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 1673 . 2  |-  F/ y
ph
2 nfv 1673 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvex 1970 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184   E.wex 1586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590
This theorem is referenced by:  eujust  2255  euind  3151  reuind  3167  cbvopab2v  4371  bm1.3ii  4421  reusv2lem2  4499  relop  4995  dmcoss  5104  fv3  5708  exfo  5866  zfun  6378  ac6sfi  7561  brwdom2  7793  aceq1  8292  aceq0  8293  aceq3lem  8295  dfac4  8297  kmlem2  8325  kmlem13  8336  axdc4lem  8629  zfac  8634  zfcndun  8787  zfcndac  8791  sup2  10291  supmul  10303  climmo  13040  summo  13199  gsumval3eu  16386  elpt  19150  usgraedg4  23310  prodmo  27454  wfrlem1  27729  frrlem1  27773  fdc  28646  axc11next  29665  fnchoice  29756  bnj1185  31792
  Copyright terms: Public domain W3C validator