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

Theorem cbvrabv 3081
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 2585 . 2  |-  F/_ x A
2 nfcv 2585 . 2  |-  F/_ y A
3 nfv 1752 . 2  |-  F/ y
ph
4 nfv 1752 . 2  |-  F/ x ps
5 cbvrabv.1 . 2  |-  ( x  =  y  ->  ( ph 
<->  ps ) )
61, 2, 3, 4, 5cbvrab 3080 1  |-  { x  e.  A  |  ph }  =  { y  e.  A  |  ps }
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    = wceq 1438   {crab 2780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-13 2054  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-ex 1661  df-nf 1665  df-sb 1788  df-clab 2409  df-cleq 2415  df-clel 2418  df-nfc 2573  df-rab 2785
This theorem is referenced by:  pwnss  4587  knatar  6261  oeeulem  7308  ordtypecbv  8036  ordtypelem9  8045  inf3lema  8133  oemapso  8190  oemapvali  8192  tz9.12lem3  8263  cofsmo  8701  enfin2i  8753  fin23lem33  8777  isf32lem11  8795  zorn2g  8935  pwfseqlem1  9085  pwfseqlem3  9087  zsupss  11255  zmin  11262  reexALT  11298  hashbc  12615  wrd2f1tovbij  13029  sqrlem7  13306  rpnnen  14272  divalglem5OLD  14369  divalglem5  14370  bitsfzolem  14400  bitsfzolemOLD  14401  smupp1  14447  gcdcllem3  14468  bezout  14503  eulerth  14724  odzval  14729  odzvalOLD  14735  pcprecl  14782  pcprendvds  14783  pcpremul  14786  pceulem  14788  prmreclem1  14853  prmreclem5  14857  prmreclem6  14858  4sqlem19  14906  vdwnn  14941  hashbcval  14947  prmgaplcmlem1OLD  15005  prmordvdslcmsOLDOLD  15014  gsumvalx  16506  symgfixelq  17067  efgsdm  17373  efgsfo  17382  ablfaclem3  17713  ltbwe  18689  coe1mul2lem2  18854  smadiadetlem3  19685  pptbas  20015  concompss  20440  ptcmplem5  21063  ustuqtop  21253  utopsnneip  21255  icccmplem2  21833  minveclem5  22367  minveclem5OLD  22379  ivth  22397  ovolicc2lem5  22467  ovolicc  22469  opnmbllem  22551  vitali  22563  itg2monolem3  22702  elqaa  23270  radcnvle  23367  pserdvlem2  23375  lgamgulmlem5  23950  lgamcvglem  23957  wilth  23988  ftalem6  23996  ttgval  24897  axcontlem11  24996  nbgraf1olem1  25161  nbgraf1o  25167  cusgraexg  25189  cusgrafi  25202  wlknwwlknbij2  25434  wlkiswwlkbij2  25441  wwlkextbij  25453  wlknwwlknvbij  25460  clwwlkvbij  25521  clwwlknscsh  25539  hashecclwwlkn1  25554  usghashecclwwlk  25555  clwlksizeeq  25572  rusgranumwlklem4  25672  rusgranumwlks  25676  frgraregorufr0  25772  usgreghash2spot  25789  extwwlkfab  25810  numclwwlk5  25832  numclwwlk7  25834  ubthlem3  26506  htth  26563  fcobijfs  28311  locfinreflem  28669  ordtconlem1  28732  dynkin  28991  ddemeas  29061  oddpwdc  29189  eulerpartgbij  29207  eulerpartlemn  29216  eulerpart  29217  ballotlemelo  29322  ballotleme  29331  ballotlem7  29370  ballotlem7OLD  29408  subfacp1lem6  29910  erdsze  29927  cvmscbv  29983  cvmsiota  30002  cvmlift2lem13  30040  neibastop2  31016  topdifinffin  31698  poimirlem27  31887  mblfinlem1  31897  mblfinlem2  31898  lclkrs2  35033  eldioph4i  35580  nzss  36530  limcperiod  37534  cncfshiftioo  37596  ioodvbdlimc1lem2  37630  ioodvbdlimc1lem2OLD  37632  ioodvbdlimc2lem  37634  ioodvbdlimc2lemOLD  37635  dvnprodlem1  37647  dvnprod  37650  itgiccshift  37683  itgperiod  37684  stoweidlem49  37736  fourierdlem41  37837  fourierdlem48  37844  fourierdlem49  37845  fourierdlem54  37850  fourierdlem65  37861  fourierdlem70  37866  fourierdlem71  37867  fourierdlem81  37877  fourierdlem89  37885  fourierdlem90  37886  fourierdlem91  37887  fourierdlem92  37888  fourierdlem96  37892  fourierdlem97  37893  fourierdlem98  37894  fourierdlem99  37895  fourierdlem100  37896  fourierdlem103  37899  fourierdlem104  37900  fourierdlem105  37901  fourierdlem108  37904  fourierdlem109  37905  fourierdlem110  37906  fourierdlem112  37908  fourierdlem113  37909  elaa2  37925  etransclem11  37936  etransc  37975  sge0fodjrnlem  38052  meadjiun  38089  ovnsubadd  38175  usgredgaleord  38932  usgedgleord  39035  usgedgleordALT  39036
  Copyright terms: Public domain W3C validator