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

Theorem cbvrabv 3112
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.)
Hypothesis
Ref Expression
cbvrabv.1  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
Assertion
Ref Expression
cbvrabv  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Distinct variable groups:    x, y, A    ph, y    ps, x
Allowed substitution hints:    ph( x)    ps( y)

Proof of Theorem cbvrabv
StepHypRef Expression
1 nfcv 2629 . 2  |-  F/_ x A
2 nfcv 2629 . 2  |-  F/_ y A
3 nfv 1683 . 2  |-  F/ y
ph
4 nfv 1683 . 2  |-  F/ x ps
5 cbvrabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvrab 3111 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1379   {crab 2818
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-rab 2823
This theorem is referenced by:  pwnss  4612  knatar  6239  oeeulem  7247  ordtypecbv  7938  ordtypelem9  7947  inf3lema  8037  oemapso  8097  oemapvali  8099  tz9.12lem3  8203  cofsmo  8645  enfin2i  8697  fin23lem33  8721  isf32lem11  8739  zorn2g  8879  pwfseqlem1  9032  pwfseqlem3  9034  zsupss  11167  zmin  11174  reexALT  11210  hashbc  12464  wrd2f1tovbij  12857  sqrlem7  13041  rpnnen  13817  divalglem5  13910  bitsfzolem  13939  smupp1  13985  gcdcllem3  14006  bezout  14035  eulerth  14168  odzval  14173  pcprecl  14218  pcprendvds  14219  pcpremul  14222  pceulem  14224  prmreclem1  14289  prmreclem5  14293  prmreclem6  14294  4sqlem19  14336  vdwnn  14371  hashbcval  14375  gsumvalx  15815  symgfixelq  16253  efgsdm  16544  efgsfo  16553  ablfaclem3  16928  ltbwe  17908  coe1mul2lem2  18080  smadiadetlem3  18937  pptbas  19275  concompss  19700  ptcmplem5  20291  ustuqtop  20484  utopsnneip  20486  icccmplem2  21063  minveclem5  21583  ivth  21601  ovolicc2lem5  21667  ovolicc  21669  opnmbllem  21745  vitali  21757  itg2monolem3  21894  elqaa  22452  radcnvle  22549  pserdvlem2  22557  wilth  23073  ftalem6  23079  ttgval  23854  axcontlem11  23953  nbgraf1olem1  24117  nbgraf1o  24123  cusgraexg  24145  cusgrafi  24158  wlknwwlknbij2  24390  wlkiswwlkbij2  24397  wwlkextbij  24409  wlknwwlknvbij  24416  clwwlkvbij  24477  clwwlknscsh  24495  hashecclwwlkn1  24510  usghashecclwwlk  24511  clwlksizeeq  24528  rusgranumwlklem4  24628  rusgranumwlks  24632  frgraregorufr0  24729  usgreghash2spot  24746  extwwlkfab  24767  numclwwlk5  24789  numclwwlk7  24791  ubthlem3  25464  htth  25511  ordtconlem1  27542  ddemeas  27848  oddpwdc  27933  eulerpartgbij  27951  eulerpartlemn  27960  eulerpart  27961  ballotlemelo  28066  ballotleme  28075  ballotlem7  28114  lgamgulmlem5  28215  lgamcvglem  28222  subfacp1lem6  28269  erdsze  28286  cvmscbv  28343  cvmsiota  28362  cvmlift2lem13  28400  mblfinlem1  29628  mblfinlem2  29629  neibastop2  29782  eldioph4i  30350  nzss  30822  cncfshiftioo  31231  ioodvbdlimc1lem2  31262  ioodvbdlimc2lem  31264  itgiccshift  31298  itgperiod  31299  stoweidlem49  31349  fourierdlem41  31448  fourierdlem48  31455  fourierdlem49  31456  fourierdlem54  31461  fourierdlem65  31472  fourierdlem70  31477  fourierdlem71  31478  fourierdlem89  31496  fourierdlem90  31497  fourierdlem91  31498  fourierdlem96  31503  fourierdlem97  31504  fourierdlem98  31505  fourierdlem99  31506  fourierdlem100  31507  fourierdlem103  31510  fourierdlem104  31511  fourierdlem105  31512  fourierdlem108  31515  fourierdlem109  31516  fourierdlem110  31517  fourierdlem112  31519  fourierdlem113  31520  usgedgleord  31888  usgedgleordALT  31889  lclkrs2  36337
  Copyright terms: Public domain W3C validator