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

Theorem cbvexv 2128
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 1772 . 2  |-  F/ y
ph
2 nfv 1772 . 2  |-  F/ x ps
3 cbvalv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
41, 2, 3cbvex 2126 1  |-  ( E. x ph  <->  E. y ps )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189   E.wex 1674
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102
This theorem depends on definitions:  df-bi 190  df-an 377  df-ex 1675  df-nf 1679
This theorem is referenced by:  eujust  2312  euind  3237  reuind  3255  cbvopab2v  4493  bm1.3ii  4544  reusv2lem2  4622  relop  5007  dmcoss  5116  fv3  5905  exfo  6068  zfun  6616  wfrlem1  7066  ac6sfi  7846  brwdom2  8119  aceq1  8579  aceq0  8580  aceq3lem  8582  dfac4  8584  kmlem2  8612  kmlem13  8623  axdc4lem  8916  zfac  8921  zfcndun  9071  zfcndac  9075  sup2  10598  supmul  10612  climmo  13676  summo  13838  prodmo  14045  gsumval3eu  17593  elpt  20642  usgraedg4  25170  bnj1185  29655  frrlem1  30564  fdc  32120  axc11next  36802  fnchoice  37391
  Copyright terms: Public domain W3C validator