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

Theorem cbvrabv 3439
 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 2158 and ax-13 2379. (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 2872 . . . 4 (𝑥 = 𝑦 → (𝑥𝐴𝑦𝐴))
2 cbvrabv.1 . . . 4 (𝑥 = 𝑦 → (𝜑𝜓))
31, 2anbi12d 633 . . 3 (𝑥 = 𝑦 → ((𝑥𝐴𝜑) ↔ (𝑦𝐴𝜓)))
43cbvabv 2866 . 2 {𝑥 ∣ (𝑥𝐴𝜑)} = {𝑦 ∣ (𝑦𝐴𝜓)}
5 df-rab 3115 . 2 {𝑥𝐴𝜑} = {𝑥 ∣ (𝑥𝐴𝜑)}
6 df-rab 3115 . 2 {𝑦𝐴𝜓} = {𝑦 ∣ (𝑦𝐴𝜓)}
74, 5, 63eqtr4i 2831 1 {𝑥𝐴𝜑} = {𝑦𝐴𝜓}
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  {cab 2776  {crab 3110 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-rab 3115 This theorem is referenced by:  rabrabi  3440  rru  3718  knatar  7089  oeeulem  8212  ordtypecbv  8967  ordtypelem9  8976  inf3lema  9073  oemapso  9131  oemapvali  9133  tz9.12lem3  9204  cofsmo  9682  enfin2i  9734  fin23lem33  9758  isf32lem11  9776  zorn2g  9916  pwfseqlem1  10071  pwfseqlem3  10073  zsupss  12327  zmin  12334  rpnnen1  12372  hashbc  13809  wrd2f1tovbij  14317  sqrlem7  14602  divalglem5  15740  bitsfzolem  15775  smupp1  15821  gcdcllem3  15842  bezout  15883  eulerth  16112  odzval  16120  pcprecl  16168  pcprendvds  16169  pcpremul  16172  pceulem  16174  prmreclem1  16244  prmreclem5  16248  prmreclem6  16249  4sqlem19  16291  vdwnn  16326  hashbcval  16330  gsumvalx  17880  symgfixelq  18556  efgsdm  18851  efgsfo  18860  ablfaclem3  19205  ltbwe  20716  coe1mul2lem2  20904  smadiadetlem3  21280  pptbas  21620  conncompss  22045  ptcmplem5  22668  ustuqtop  22859  utopsnneip  22861  icccmplem2  23435  minveclem5  24044  ivth  24065  ovolicc2lem5  24132  ovolicc  24134  opnmbllem  24212  vitali  24224  itg2monolem3  24363  elqaa  24925  radcnvle  25022  pserdvlem2  25030  lgamgulmlem5  25625  lgamcvglem  25632  wilth  25663  ftalem6  25670  ttgval  26676  axcontlem11  26775  lfgredgge2  26924  usgredgleordALT  27031  nbusgrf1o  27168  cusgrexg  27241  cusgrfilem2  27253  cusgrfi  27255  vtxdushgrfvedglem  27286  vtxdushgrfvedg  27287  vtxdginducedm1  27340  finsumvtxdg2sstep  27346  wwlksnextbij  27695  rusgrnumwwlks  27767  clwlkclwwlkfolem  27799  clwlkclwwlken  27804  clwwlknscsh  27854  hashecclwwlkn1  27869  umgrhashecclwwlk  27870  clwlknf1oclwwlknlem2  27874  clwlknf1oclwwlkn  27876  frgrwopreglem5lem  28112  frgrregorufr0  28116  fusgreghash2wsp  28130  dlwwlknondlwlknonf1o  28157  ubthlem3  28662  htth  28708  fcobijfs  30492  locfinreflem  31205  zarmxt1  31245  zarcmp  31247  ordtconnlem1  31289  dynkin  31548  ddemeas  31617  oddpwdc  31734  eulerpartgbij  31752  eulerpartlemn  31761  eulerpart  31762  ballotlemelo  31867  ballotleme  31876  ballotlem7  31915  reprsuc  32008  hgt750lema  32050  hgt750leme  32051  subfacp1lem6  32557  erdsze  32574  cvmscbv  32630  cvmsiota  32649  cvmlift2lem13  32687  satfv1  32735  neibastop2  33834  topdifinffin  34781  poimirlem27  35100  mblfinlem1  35110  mblfinlem2  35111  lclkrs2  38852  eldioph4i  39768  rfovcnvf1od  40720  fsovrfovd  40725  fsovcnvlem  40729  nzss  41036  supminfxr2  42123  limcperiod  42285  cncfshiftioo  42549  ioodvbdlimc1lem2  42589  ioodvbdlimc2lem  42591  dvnprodlem1  42603  dvnprod  42606  itgiccshift  42637  itgperiod  42638  stoweidlem49  42706  fourierdlem41  42805  fourierdlem48  42811  fourierdlem49  42812  fourierdlem54  42817  fourierdlem65  42828  fourierdlem70  42833  fourierdlem71  42834  fourierdlem81  42844  fourierdlem89  42852  fourierdlem90  42853  fourierdlem91  42854  fourierdlem92  42855  fourierdlem96  42859  fourierdlem97  42860  fourierdlem98  42861  fourierdlem99  42862  fourierdlem100  42863  fourierdlem103  42866  fourierdlem104  42867  fourierdlem105  42868  fourierdlem108  42871  fourierdlem109  42872  fourierdlem110  42873  fourierdlem112  42875  fourierdlem113  42876  elaa2  42891  etransclem11  42902  etransc  42940  salexct  42989  subsaliuncl  43013  sge0fodjrnlem  43070  meadjiun  43120  ovnsubadd  43226  hoidmv1le  43248  hoidmvlelem3  43251  hoidmvlelem5  43253  ovnhoi  43257  hspmbllem3  43282  hspmbl  43283  opnvonmbl  43288  ovolval4lem2  43304  ovolval5lem2  43307  ovolval5lem3  43308  ovolval5  43309  ovnovol  43313  issmf  43377  incsmf  43391  issmfle  43394  issmfgt  43405  smfadd  43413  decsmf  43415  issmfge  43418  smflimlem4  43422  smflim  43425  smfmul  43442  smflimsuplem2  43467  smflimsuplem5  43470  smflimsuplem7  43472  requad2  44156
 Copyright terms: Public domain W3C validator