Theorem cbvrabv 3199

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

Step	Hyp	Ref	Expression
1		nfcv 2764	. 2 |- F/_ x A
2		nfcv 2764	. 2 |- F/_ y A
3		nfv 1843	. 2 |- F/ y ph
4		nfv 1843	. 2 |- F/ x ps
5		cbvrabv.1	. 2 |- ( x = y -> ( ph <-> ps ) )
6	1, 2, 3, 4, 5	cbvrab 3198	1 |- { x e. A | ph } = { y e. A | ps }

Syntax hints:   -> wi 4   <-> wb 196   = wceq 1483   {crab 2916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-rab 2921

This theorem is referenced by:  pwnss  4830  knatar  6607  oeeulem  7681  ordtypecbv  8422  ordtypelem9  8431  inf3lema  8521  oemapso  8579  oemapvali  8581  tz9.12lem3  8652  cofsmo  9091  enfin2i  9143  fin23lem33  9167  isf32lem11  9185  zorn2g  9325  pwfseqlem1  9480  pwfseqlem3  9482  zsupss  11777  zmin  11784  rpnnen1  11820  hashbc  13237  wrd2f1tovbij  13703  sqrlem7  13989  divalglem5  15120  bitsfzolem  15156  smupp1  15202  gcdcllem3  15223  bezout  15260  eulerth  15488  odzval  15496  pcprecl  15544  pcprendvds  15545  pcpremul  15548  pceulem  15550  prmreclem1  15620  prmreclem5  15624  prmreclem6  15625  4sqlem19  15667  vdwnn  15702  hashbcval  15706  gsumvalx  17270  symgfixelq  17853  efgsdm  18143  efgsfo  18152  ablfaclem3  18486  ltbwe  19472  coe1mul2lem2  19638  smadiadetlem3  20474  pptbas  20812  conncompss  21236  ptcmplem5  21860  ustuqtop  22050  utopsnneip  22052  icccmplem2  22626  minveclem5  23204  ivth  23223  ovolicc2lem5  23289  ovolicc  23291  opnmbllem  23369  vitali  23382  itg2monolem3  23519  elqaa  24077  radcnvle  24174  pserdvlem2  24182  lgamgulmlem5  24759  lgamcvglem  24766  wilth  24797  ftalem6  24804  ttgval  25755  axcontlem11  25854  lfgredgge2  26019  usgredgleordALT  26126  nbusgrf1o  26273  cusgrexg  26340  cusgrfilem2  26352  cusgrfi  26354  vtxdushgrfvedglem  26385  vtxdushgrfvedg  26386  vtxdginducedm1  26439  finsumvtxdg2sstep  26445  wlknwwlksnbij2  26778  wlkwwlkbij2  26785  wwlksnextbij  26797  wlksnwwlknvbij  26803  rusgrnumwwlks  26869  clwwlksvbij  26922  clwwlksnscsh  26940  hashecclwwlksn1  26954  umgrhashecclwwlk  26955  clwlkssizeeq  26971  frgrwopreglem5lem  27184  frgrregorufr0  27188  fusgreghash2wsp  27202  extwwlkfab  27223  numclwwlk6  27248  ubthlem3  27728  htth  27775  fcobijfs  29501  locfinreflem  29907  ordtconnlem1  29970  dynkin  30230  ddemeas  30299  oddpwdc  30416  eulerpartgbij  30434  eulerpartlemn  30443  eulerpart  30444  ballotlemelo  30549  ballotleme  30558  ballotlem7  30597  reprsuc  30693  hgt750lema  30735  hgt750leme  30736  subfacp1lem6  31167  erdsze  31184  cvmscbv  31240  cvmsiota  31259  cvmlift2lem13  31297  neibastop2  32356  topdifinffin  33196  poimirlem27  33436  mblfinlem1  33446  mblfinlem2  33447  lclkrs2  36829  eldioph4i  37376  rfovcnvf1od  38298  fsovrfovd  38303  fsovcnvlem  38307  nzss  38516  supminfxr2  39699  limcperiod  39860  cncfshiftioo  40105  ioodvbdlimc1lem2  40147  ioodvbdlimc2lem  40149  dvnprodlem1  40161  dvnprod  40164  itgiccshift  40196  itgperiod  40197  stoweidlem49  40266  fourierdlem41  40365  fourierdlem48  40371  fourierdlem49  40372  fourierdlem54  40377  fourierdlem65  40388  fourierdlem70  40393  fourierdlem71  40394  fourierdlem81  40404  fourierdlem89  40412  fourierdlem90  40413  fourierdlem91  40414  fourierdlem92  40415  fourierdlem96  40419  fourierdlem97  40420  fourierdlem98  40421  fourierdlem99  40422  fourierdlem100  40423  fourierdlem103  40426  fourierdlem104  40427  fourierdlem105  40428  fourierdlem108  40431  fourierdlem109  40432  fourierdlem110  40433  fourierdlem112  40435  fourierdlem113  40436  elaa2  40451  etransclem11  40462  etransc  40500  salexct  40552  subsaliuncl  40576  sge0fodjrnlem  40633  meadjiun  40683  ovnsubadd  40786  hoidmv1le  40808  hoidmvlelem3  40811  hoidmvlelem5  40813  ovnhoi  40817  hspmbllem3  40842  hspmbl  40843  opnvonmbl  40848  ovolval4lem2  40864  ovolval5lem2  40867  ovolval5lem3  40868  ovolval5  40869  ovnovol  40873  issmf  40937  incsmf  40951  issmfle  40954  issmfgt  40965  smfadd  40973  decsmf  40975  issmfge  40978  smflimlem4  40982  smflim  40985  smfmul  41002  smflimsuplem2  41027  smflimsuplem5  41030  smflimsuplem7  41032