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

Theorem cbvrabv 3030
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 2612 . 2  |-  F/_ x A
2 nfcv 2612 . 2  |-  F/_ y A
3 nfv 1769 . 2  |-  F/ y
ph
4 nfv 1769 . 2  |-  F/ x ps
5 cbvrabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvrab 3029 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    = wceq 1452   {crab 2760
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-rab 2765
This theorem is referenced by:  pwnss  4566  knatar  6266  oeeulem  7320  ordtypecbv  8050  ordtypelem9  8059  inf3lema  8147  oemapso  8205  oemapvali  8207  tz9.12lem3  8278  cofsmo  8717  enfin2i  8769  fin23lem33  8793  isf32lem11  8811  zorn2g  8951  pwfseqlem1  9101  pwfseqlem3  9103  zsupss  11276  zmin  11283  reexALT  11319  hashbc  12657  wrd2f1tovbij  13110  sqrlem7  13389  rpnnen  14356  divalglem5OLD  14455  divalglem5  14456  bitsfzolem  14486  bitsfzolemOLD  14487  smupp1  14533  gcdcllem3  14554  bezout  14589  eulerth  14810  odzval  14815  odzvalOLD  14821  pcprecl  14868  pcprendvds  14869  pcpremul  14872  pceulem  14874  prmreclem1  14939  prmreclem5  14943  prmreclem6  14944  4sqlem19  14992  vdwnn  15027  hashbcval  15033  prmgaplcmlem1OLD  15091  prmordvdslcmsOLDOLD  15100  gsumvalx  16591  symgfixelq  17152  efgsdm  17458  efgsfo  17467  ablfaclem3  17798  ltbwe  18773  coe1mul2lem2  18938  smadiadetlem3  19770  pptbas  20100  concompss  20525  ptcmplem5  21149  ustuqtop  21339  utopsnneip  21341  icccmplem2  21919  minveclem5  22453  minveclem5OLD  22465  ivth  22483  ovolicc2lem5  22553  ovolicc  22555  opnmbllem  22638  vitali  22650  itg2monolem3  22789  elqaa  23357  radcnvle  23454  pserdvlem2  23462  lgamgulmlem5  24037  lgamcvglem  24044  wilth  24075  ftalem6  24083  ttgval  24984  axcontlem11  25083  nbgraf1olem1  25248  nbgraf1o  25254  cusgraexg  25276  cusgrafi  25289  wlknwwlknbij2  25521  wlkiswwlkbij2  25528  wwlkextbij  25540  wlknwwlknvbij  25547  clwwlkvbij  25608  clwwlknscsh  25626  hashecclwwlkn1  25641  usghashecclwwlk  25642  clwlksizeeq  25659  rusgranumwlklem4  25759  rusgranumwlks  25763  frgraregorufr0  25859  usgreghash2spot  25876  extwwlkfab  25897  numclwwlk5  25919  numclwwlk7  25921  ubthlem3  26595  htth  26652  fcobijfs  28386  locfinreflem  28741  ordtconlem1  28804  dynkin  29063  ddemeas  29132  oddpwdc  29260  eulerpartgbij  29278  eulerpartlemn  29287  eulerpart  29288  ballotlemelo  29393  ballotleme  29402  ballotlem7  29441  ballotlem7OLD  29479  subfacp1lem6  29980  erdsze  29997  cvmscbv  30053  cvmsiota  30072  cvmlift2lem13  30110  neibastop2  31088  topdifinffin  31821  poimirlem27  32031  mblfinlem1  32041  mblfinlem2  32042  lclkrs2  35179  eldioph4i  35726  nzss  36736  limcperiod  37805  cncfshiftioo  37867  ioodvbdlimc1lem2  37901  ioodvbdlimc1lem2OLD  37903  ioodvbdlimc2lem  37905  ioodvbdlimc2lemOLD  37906  dvnprodlem1  37918  dvnprod  37921  itgiccshift  37954  itgperiod  37955  stoweidlem49  38022  fourierdlem41  38123  fourierdlem48  38130  fourierdlem49  38131  fourierdlem54  38136  fourierdlem65  38147  fourierdlem70  38152  fourierdlem71  38153  fourierdlem81  38163  fourierdlem89  38171  fourierdlem90  38172  fourierdlem91  38173  fourierdlem92  38174  fourierdlem96  38178  fourierdlem97  38179  fourierdlem98  38180  fourierdlem99  38181  fourierdlem100  38182  fourierdlem103  38185  fourierdlem104  38186  fourierdlem105  38187  fourierdlem108  38190  fourierdlem109  38191  fourierdlem110  38192  fourierdlem112  38194  fourierdlem113  38195  elaa2  38211  etransclem11  38222  etransc  38261  salexct  38305  sge0fodjrnlem  38372  meadjiun  38420  ovnsubadd  38512  hoidmv1le  38534  hoidmvlelem3  38537  hoidmvlelem5  38539  ovnhoi  38543  hspmbllem3  38568  hspmbl  38569  opnvonmbl  38574  ovolval4lem2  38590  ovolval5lem2  38593  ovolval5lem3  38594  ovolval5  38595  ovnovol  38599  lfgredgge2  39369  usgredgaleordALT  39475  nbusgrf1o  39609  cusgrexg  39673  cusgrfilem2  39682  cusgrfi  39684  vtxdushgrfvedglem  39712  vtxdushgrfvedg  39713  usgedgleord  40239  usgedgleordALT  40240
  Copyright terms: Public domain W3C validator