Theorem cbvrabv 3413

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 2370. (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 2811	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2799	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3403	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3403	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2762	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2707  {crab 3402

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3403

This theorem is referenced by:  rru  3747  knatar  7314  oeeulem  8542  cofon1  8613  ordtypecbv  9446  ordtypelem9  9455  inf3lema  9553  oemapso  9611  oemapvali  9613  tz9.12lem3  9718  cofsmo  10198  enfin2i  10250  fin23lem33  10274  isf32lem11  10292  zorn2g  10432  pwfseqlem1  10587  pwfseqlem3  10589  zsupss  12872  zmin  12879  rpnnen1  12918  hashbc  14394  wrd2f1tovbij  14902  01sqrexlem7  15190  divalglem5  16343  bitsfzolem  16380  smupp1  16426  gcdcllem3  16447  bezout  16489  eulerth  16729  odzval  16738  pcprecl  16786  pcprendvds  16787  pcpremul  16790  pceulem  16792  prmreclem1  16863  prmreclem5  16867  prmreclem6  16868  4sqlem19  16910  vdwnn  16945  hashbcval  16949  gsumvalx  18579  symgfixelq  19339  efgsdm  19636  efgsfo  19645  ablfaclem3  19995  ltbwe  21927  coe1mul2lem2  22130  smadiadetlem3  22531  pptbas  22871  conncompss  23296  ptcmplem5  23919  ustuqtop  24110  utopsnneip  24112  icccmplem2  24688  minveclem5  25309  ivth  25331  ovolicc2lem5  25398  ovolicc  25400  opnmbllem  25478  vitali  25490  itg2monolem3  25629  elqaa  26206  radcnvle  26305  pserdvlem2  26314  lgamgulmlem5  26919  lgamcvglem  26926  wilth  26957  ftalem6  26964  precsexlemcbv  28084  bdayon  28149  ttgval  28778  axcontlem11  28877  lfgredgge2  29027  usgredgleordALT  29137  nbusgrf1o  29274  cusgrexg  29347  cusgrfilem2  29360  cusgrfi  29362  vtxdushgrfvedglem  29393  vtxdushgrfvedg  29394  vtxdginducedm1  29447  finsumvtxdg2sstep  29453  wwlksnextbij  29805  rusgrnumwwlks  29877  clwlkclwwlkfolem  29909  clwlkclwwlken  29914  clwwlknscsh  29964  hashecclwwlkn1  29979  umgrhashecclwwlk  29980  clwlknf1oclwwlknlem2  29984  clwlknf1oclwwlkn  29986  frgrwopreglem5lem  30222  frgrregorufr0  30226  fusgreghash2wsp  30240  dlwwlknondlwlknonf1o  30267  ubthlem3  30774  htth  30820  fcobijfs  32619  elrgspnsubrunlem1  33171  elrgspnsubrun  33173  1arithufd  33492  constrsuc  33701  constrcbvlem  33718  locfinreflem  33803  zarmxt1  33843  zarcmp  33845  ordtconnlem1  33887  dynkin  34130  ddemeas  34199  oddpwdc  34318  eulerpartgbij  34336  eulerpartlemn  34345  eulerpart  34346  ballotlemelo  34452  ballotleme  34461  ballotlem7  34500  reprsuc  34579  hgt750lema  34621  hgt750leme  34622  onvf1odlem3  35065  subfacp1lem6  35145  erdsze  35162  cvmscbv  35218  cvmsiota  35237  cvmlift2lem13  35275  satfv1  35323  neibastop2  36322  weiunfrlem  36425  topdifinffin  37309  poimirlem27  37614  mblfinlem1  37624  mblfinlem2  37625  lclkrs2  41507  aks4d1  42050  sticksstones2  42108  eldioph4i  42773  rfovcnvf1od  43966  fsovrfovd  43971  fsovcnvlem  43975  nzss  44279  supminfxr2  45438  limcperiod  45599  cncfshiftioo  45863  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnprodlem1  45917  dvnprod  45920  itgiccshift  45951  itgperiod  45952  stoweidlem49  46020  fourierdlem41  46119  fourierdlem48  46125  fourierdlem49  46126  fourierdlem54  46131  fourierdlem65  46142  fourierdlem70  46147  fourierdlem71  46148  fourierdlem81  46158  fourierdlem89  46166  fourierdlem90  46167  fourierdlem91  46168  fourierdlem92  46169  fourierdlem96  46173  fourierdlem97  46174  fourierdlem98  46175  fourierdlem99  46176  fourierdlem100  46177  fourierdlem103  46180  fourierdlem104  46181  fourierdlem105  46182  fourierdlem108  46185  fourierdlem109  46186  fourierdlem110  46187  fourierdlem112  46189  fourierdlem113  46190  elaa2  46205  etransclem11  46216  etransc  46254  salexct  46305  subsaliuncl  46329  sge0fodjrnlem  46387  meadjiun  46437  ovnsubadd  46543  hoidmv1le  46565  hoidmvlelem3  46568  hoidmvlelem5  46570  ovnhoi  46574  hspmbllem3  46599  hspmbl  46600  opnvonmbl  46605  ovolval4lem2  46621  ovolval5lem2  46624  ovolval5lem3  46625  ovolval5  46626  ovnovol  46630  issmf  46699  incsmf  46713  issmfle  46716  issmfgt  46727  smfadd  46736  decsmf  46738  issmfge  46741  smflimlem4  46745  smflim  46748  smfmul  46766  smflimsuplem2  46792  smflimsuplem5  46795  smflimsuplem7  46797  requad2  47597  uspgrlimlem1  47960  grlimgrtri  47968  gpgusgralem  48020  intubeu  48945  unilbeu  48946