Theorem cbvrabv 3430

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 2147 and ax-13 2366. (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

Step	Hyp	Ref	Expression
1		eleq1w 2809	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 630	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2799	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3420	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3420	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2764	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   = wceq 1534   ∈ wcel 2099  {cab 2703  {crab 3419

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2697

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1775  df-sb 2061  df-clab 2704  df-cleq 2718  df-clel 2803  df-rab 3420

This theorem is referenced by:  rabrabiOLD  3444  rru  3773  knatar  7369  oeeulem  8631  cofon1  8702  ordtypecbv  9560  ordtypelem9  9569  inf3lema  9667  oemapso  9725  oemapvali  9727  tz9.12lem3  9832  cofsmo  10312  enfin2i  10364  fin23lem33  10388  isf32lem11  10406  zorn2g  10546  pwfseqlem1  10701  pwfseqlem3  10703  zsupss  12973  zmin  12980  rpnnen1  13019  hashbc  14470  wrd2f1tovbij  14969  01sqrexlem7  15253  divalglem5  16399  bitsfzolem  16434  smupp1  16480  gcdcllem3  16501  bezout  16544  eulerth  16785  odzval  16793  pcprecl  16841  pcprendvds  16842  pcpremul  16845  pceulem  16847  prmreclem1  16918  prmreclem5  16922  prmreclem6  16923  4sqlem19  16965  vdwnn  17000  hashbcval  17004  gsumvalx  18669  symgfixelq  19431  efgsdm  19728  efgsfo  19737  ablfaclem3  20087  ltbwe  22051  coe1mul2lem2  22259  smadiadetlem3  22661  pptbas  23002  conncompss  23428  ptcmplem5  24051  ustuqtop  24242  utopsnneip  24244  icccmplem2  24830  minveclem5  25452  ivth  25474  ovolicc2lem5  25541  ovolicc  25543  opnmbllem  25621  vitali  25633  itg2monolem3  25773  elqaa  26350  radcnvle  26449  pserdvlem2  26458  lgamgulmlem5  27061  lgamcvglem  27068  wilth  27099  ftalem6  27106  precsexlemcbv  28205  ttgval  28802  ttgvalOLD  28803  axcontlem11  28908  lfgredgge2  29060  usgredgleordALT  29170  nbusgrf1o  29307  cusgrexg  29380  cusgrfilem2  29393  cusgrfi  29395  vtxdushgrfvedglem  29426  vtxdushgrfvedg  29427  vtxdginducedm1  29480  finsumvtxdg2sstep  29486  wwlksnextbij  29836  rusgrnumwwlks  29908  clwlkclwwlkfolem  29940  clwlkclwwlken  29945  clwwlknscsh  29995  hashecclwwlkn1  30010  umgrhashecclwwlk  30011  clwlknf1oclwwlknlem2  30015  clwlknf1oclwwlkn  30017  frgrwopreglem5lem  30253  frgrregorufr0  30257  fusgreghash2wsp  30271  dlwwlknondlwlknonf1o  30298  ubthlem3  30805  htth  30851  fcobijfs  32637  1arithufd  33423  constrsuc  33596  locfinreflem  33655  zarmxt1  33695  zarcmp  33697  ordtconnlem1  33739  dynkin  34000  ddemeas  34069  oddpwdc  34188  eulerpartgbij  34206  eulerpartlemn  34215  eulerpart  34216  ballotlemelo  34321  ballotleme  34330  ballotlem7  34369  reprsuc  34461  hgt750lema  34503  hgt750leme  34504  subfacp1lem6  35013  erdsze  35030  cvmscbv  35086  cvmsiota  35105  cvmlift2lem13  35143  satfv1  35191  neibastop2  36073  topdifinffin  37055  poimirlem27  37348  mblfinlem1  37358  mblfinlem2  37359  lclkrs2  41239  aks4d1  41788  sticksstones2  41845  eldioph4i  42469  rfovcnvf1od  43671  fsovrfovd  43676  fsovcnvlem  43680  nzss  43991  supminfxr2  45084  limcperiod  45249  cncfshiftioo  45513  ioodvbdlimc1lem2  45553  ioodvbdlimc2lem  45555  dvnprodlem1  45567  dvnprod  45570  itgiccshift  45601  itgperiod  45602  stoweidlem49  45670  fourierdlem41  45769  fourierdlem48  45775  fourierdlem49  45776  fourierdlem54  45781  fourierdlem65  45792  fourierdlem70  45797  fourierdlem71  45798  fourierdlem81  45808  fourierdlem89  45816  fourierdlem90  45817  fourierdlem91  45818  fourierdlem92  45819  fourierdlem96  45823  fourierdlem97  45824  fourierdlem98  45825  fourierdlem99  45826  fourierdlem100  45827  fourierdlem103  45830  fourierdlem104  45831  fourierdlem105  45832  fourierdlem108  45835  fourierdlem109  45836  fourierdlem110  45837  fourierdlem112  45839  fourierdlem113  45840  elaa2  45855  etransclem11  45866  etransc  45904  salexct  45955  subsaliuncl  45979  sge0fodjrnlem  46037  meadjiun  46087  ovnsubadd  46193  hoidmv1le  46215  hoidmvlelem3  46218  hoidmvlelem5  46220  ovnhoi  46224  hspmbllem3  46249  hspmbl  46250  opnvonmbl  46255  ovolval4lem2  46271  ovolval5lem2  46274  ovolval5lem3  46275  ovolval5  46276  ovnovol  46280  issmf  46349  incsmf  46363  issmfle  46366  issmfgt  46377  smfadd  46386  decsmf  46388  issmfge  46391  smflimlem4  46395  smflim  46398  smfmul  46416  smflimsuplem2  46442  smflimsuplem5  46445  smflimsuplem7  46447  requad2  47195  intubeu  48310  unilbeu  48311