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

Theorem cbvrabv 3492
Description: Rule to change the bound variable in a restricted class abstraction, using implicit substitution. (Contributed by NM, 26-May-1999.) Require 𝑥, 𝑦 be disjoint to avoid ax-11 2151 and ax-13 2383. (Revised by Steven Nguyen, 4-Dec-2022.)
Hypothesis
Ref Expression
cbvrabv.1 (𝑥 = 𝑦 → (𝜑𝜓))
Assertion
Ref Expression
cbvrabv {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Distinct variable groups:   𝑥,𝑦,𝐴   𝜑,𝑦   𝜓,𝑥
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)

Proof of Theorem cbvrabv
StepHypRef Expression
1 eleq1w 2895 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2 cbvrabv.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2anbi12d 630 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
43cbvabv 2889 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
5 df-rab 3147 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
6 df-rab 3147 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
74, 5, 63eqtr4i 2854 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1528  wcel 2105  {cab 2799  {crab 3142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-rab 3147
This theorem is referenced by:  rabrabi  3494  rru  3769  knatar  7099  oeeulem  8217  ordtypecbv  8970  ordtypelem9  8979  inf3lema  9076  oemapso  9134  oemapvali  9136  tz9.12lem3  9207  cofsmo  9680  enfin2i  9732  fin23lem33  9756  isf32lem11  9774  zorn2g  9914  pwfseqlem1  10069  pwfseqlem3  10071  zsupss  12326  zmin  12333  rpnnen1  12372  hashbc  13801  wrd2f1tovbij  14314  sqrlem7  14598  divalglem5  15738  bitsfzolem  15773  smupp1  15819  gcdcllem3  15840  bezout  15881  eulerth  16110  odzval  16118  pcprecl  16166  pcprendvds  16167  pcpremul  16170  pceulem  16172  prmreclem1  16242  prmreclem5  16246  prmreclem6  16247  4sqlem19  16289  vdwnn  16324  hashbcval  16328  gsumvalx  17876  symgfixelq  18492  efgsdm  18787  efgsfo  18796  ablfaclem3  19140  ltbwe  20183  coe1mul2lem2  20366  smadiadetlem3  21207  pptbas  21546  conncompss  21971  ptcmplem5  22594  ustuqtop  22784  utopsnneip  22786  icccmplem2  23360  minveclem5  23965  ivth  23984  ovolicc2lem5  24051  ovolicc  24053  opnmbllem  24131  vitali  24143  itg2monolem3  24282  elqaa  24840  radcnvle  24937  pserdvlem2  24945  lgamgulmlem5  25538  lgamcvglem  25545  wilth  25576  ftalem6  25583  ttgval  26589  axcontlem11  26688  lfgredgge2  26837  usgredgleordALT  26944  nbusgrf1o  27081  cusgrexg  27154  cusgrfilem2  27166  cusgrfi  27168  vtxdushgrfvedglem  27199  vtxdushgrfvedg  27200  vtxdginducedm1  27253  finsumvtxdg2sstep  27259  wwlksnextbij  27608  rusgrnumwwlks  27681  clwlkclwwlkfolem  27713  clwlkclwwlken  27718  clwwlknscsh  27769  hashecclwwlkn1  27784  umgrhashecclwwlk  27785  clwlknf1oclwwlknlem2  27789  clwlknf1oclwwlkn  27791  frgrwopreglem5lem  28027  frgrregorufr0  28031  fusgreghash2wsp  28045  dlwwlknondlwlknonf1o  28072  ubthlem3  28577  htth  28623  fcobijfs  30386  locfinreflem  31004  ordtconnlem1  31067  dynkin  31326  ddemeas  31395  oddpwdc  31512  eulerpartgbij  31530  eulerpartlemn  31539  eulerpart  31540  ballotlemelo  31645  ballotleme  31654  ballotlem7  31693  reprsuc  31786  hgt750lema  31828  hgt750leme  31829  subfacp1lem6  32330  erdsze  32347  cvmscbv  32403  cvmsiota  32422  cvmlift2lem13  32460  satfv1  32508  neibastop2  33607  topdifinffin  34512  poimirlem27  34801  mblfinlem1  34811  mblfinlem2  34812  lclkrs2  38558  eldioph4i  39289  rfovcnvf1od  40230  fsovrfovd  40235  fsovcnvlem  40239  nzss  40529  supminfxr2  41625  limcperiod  41789  cncfshiftioo  42055  ioodvbdlimc1lem2  42097  ioodvbdlimc2lem  42099  dvnprodlem1  42111  dvnprod  42114  itgiccshift  42145  itgperiod  42146  stoweidlem49  42215  fourierdlem41  42314  fourierdlem48  42320  fourierdlem49  42321  fourierdlem54  42326  fourierdlem65  42337  fourierdlem70  42342  fourierdlem71  42343  fourierdlem81  42353  fourierdlem89  42361  fourierdlem90  42362  fourierdlem91  42363  fourierdlem92  42364  fourierdlem96  42368  fourierdlem97  42369  fourierdlem98  42370  fourierdlem99  42371  fourierdlem100  42372  fourierdlem103  42375  fourierdlem104  42376  fourierdlem105  42377  fourierdlem108  42380  fourierdlem109  42381  fourierdlem110  42382  fourierdlem112  42384  fourierdlem113  42385  elaa2  42400  etransclem11  42411  etransc  42449  salexct  42498  subsaliuncl  42522  sge0fodjrnlem  42579  meadjiun  42629  ovnsubadd  42735  hoidmv1le  42757  hoidmvlelem3  42760  hoidmvlelem5  42762  ovnhoi  42766  hspmbllem3  42791  hspmbl  42792  opnvonmbl  42797  ovolval4lem2  42813  ovolval5lem2  42816  ovolval5lem3  42817  ovolval5  42818  ovnovol  42822  issmf  42886  incsmf  42900  issmfle  42903  issmfgt  42914  smfadd  42922  decsmf  42924  issmfge  42927  smflimlem4  42931  smflim  42934  smfmul  42951  smflimsuplem2  42976  smflimsuplem5  42979  smflimsuplem7  42981  requad2  43635
  Copyright terms: Public domain W3C validator