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

Theorem cbvrabv 3230
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 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvrabv {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrabv
StepHypRef Expression
1 nfcv 2793 . 2 𝑥𝐴
2 nfcv 2793 . 2 𝑦𝐴
3 nfv 1883 . 2 𝑦𝜑
4 nfv 1883 . 2 𝑥𝜓
5 cbvrabv.1 . 2 (𝑥 = 𝑦 → (𝜑𝜓))
61, 2, 3, 4, 5cbvrab 3229 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196   = wceq 1523  {crab 2945
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950
This theorem is referenced by:  pwnss  4860  knatar  6647  oeeulem  7726  ordtypecbv  8463  ordtypelem9  8472  inf3lema  8559  oemapso  8617  oemapvali  8619  tz9.12lem3  8690  cofsmo  9129  enfin2i  9181  fin23lem33  9205  isf32lem11  9223  zorn2g  9363  pwfseqlem1  9518  pwfseqlem3  9520  zsupss  11815  zmin  11822  rpnnen1  11858  hashbc  13275  wrd2f1tovbij  13749  sqrlem7  14033  divalglem5  15167  bitsfzolem  15203  smupp1  15249  gcdcllem3  15270  bezout  15307  eulerth  15535  odzval  15543  pcprecl  15591  pcprendvds  15592  pcpremul  15595  pceulem  15597  prmreclem1  15667  prmreclem5  15671  prmreclem6  15672  4sqlem19  15714  vdwnn  15749  hashbcval  15753  gsumvalx  17317  symgfixelq  17899  efgsdm  18189  efgsfo  18198  ablfaclem3  18532  ltbwe  19520  coe1mul2lem2  19686  smadiadetlem3  20522  pptbas  20860  conncompss  21284  ptcmplem5  21907  ustuqtop  22097  utopsnneip  22099  icccmplem2  22673  minveclem5  23250  ivth  23269  ovolicc2lem5  23335  ovolicc  23337  opnmbllem  23415  vitali  23427  itg2monolem3  23564  elqaa  24122  radcnvle  24219  pserdvlem2  24227  lgamgulmlem5  24804  lgamcvglem  24811  wilth  24842  ftalem6  24849  ttgval  25800  axcontlem11  25899  lfgredgge2  26064  usgredgleordALT  26171  nbusgrf1o  26317  cusgrexg  26396  cusgrfilem2  26408  cusgrfi  26410  vtxdushgrfvedglem  26441  vtxdushgrfvedg  26442  vtxdginducedm1  26495  finsumvtxdg2sstep  26501  wlknwwlksnbij2  26846  wlkwwlkbij2  26853  wwlksnextbij  26865  wlksnwwlknvbij  26871  rusgrnumwwlks  26941  clwwlknscsh  27027  hashecclwwlkn1  27041  umgrhashecclwwlk  27042  clwlkssizeeq  27058  clwwlkvbijOLD  27089  frgrwopreglem5lem  27300  frgrregorufr0  27304  fusgreghash2wsp  27318  ubthlem3  27856  htth  27903  fcobijfs  29629  locfinreflem  30035  ordtconnlem1  30098  dynkin  30358  ddemeas  30427  oddpwdc  30544  eulerpartgbij  30562  eulerpartlemn  30571  eulerpart  30572  ballotlemelo  30677  ballotleme  30686  ballotlem7  30725  reprsuc  30821  hgt750lema  30863  hgt750leme  30864  subfacp1lem6  31293  erdsze  31310  cvmscbv  31366  cvmsiota  31385  cvmlift2lem13  31423  neibastop2  32481  topdifinffin  33326  poimirlem27  33566  mblfinlem1  33576  mblfinlem2  33577  lclkrs2  37146  eldioph4i  37693  rfovcnvf1od  38615  fsovrfovd  38620  fsovcnvlem  38624  nzss  38833  supminfxr2  40012  limcperiod  40178  cncfshiftioo  40423  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnprodlem1  40479  dvnprod  40482  itgiccshift  40514  itgperiod  40515  stoweidlem49  40584  fourierdlem41  40683  fourierdlem48  40689  fourierdlem49  40690  fourierdlem54  40695  fourierdlem65  40706  fourierdlem70  40711  fourierdlem71  40712  fourierdlem81  40722  fourierdlem89  40730  fourierdlem90  40731  fourierdlem91  40732  fourierdlem92  40733  fourierdlem96  40737  fourierdlem97  40738  fourierdlem98  40739  fourierdlem99  40740  fourierdlem100  40741  fourierdlem103  40744  fourierdlem104  40745  fourierdlem105  40746  fourierdlem108  40749  fourierdlem109  40750  fourierdlem110  40751  fourierdlem112  40753  fourierdlem113  40754  elaa2  40769  etransclem11  40780  etransc  40818  salexct  40870  subsaliuncl  40894  sge0fodjrnlem  40951  meadjiun  41001  ovnsubadd  41107  hoidmv1le  41129  hoidmvlelem3  41132  hoidmvlelem5  41134  ovnhoi  41138  hspmbllem3  41163  hspmbl  41164  opnvonmbl  41169  ovolval4lem2  41185  ovolval5lem2  41188  ovolval5lem3  41189  ovolval5  41190  ovnovol  41194  issmf  41258  incsmf  41272  issmfle  41275  issmfgt  41286  smfadd  41294  decsmf  41296  issmfge  41299  smflimlem4  41303  smflim  41306  smfmul  41323  smflimsuplem2  41348  smflimsuplem5  41351  smflimsuplem7  41353
  Copyright terms: Public domain W3C validator