Theorem cbvrabv 3407

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 3397	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3397	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2762	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

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

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 3397

This theorem is referenced by:  rru  3741  knatar  7298  oeeulem  8526  cofon1  8597  ordtypecbv  9428  ordtypelem9  9437  inf3lema  9539  oemapso  9597  oemapvali  9599  tz9.12lem3  9704  cofsmo  10182  enfin2i  10234  fin23lem33  10258  isf32lem11  10276  zorn2g  10416  pwfseqlem1  10571  pwfseqlem3  10573  zsupss  12856  zmin  12863  rpnnen1  12902  hashbc  14378  wrd2f1tovbij  14885  01sqrexlem7  15173  divalglem5  16326  bitsfzolem  16363  smupp1  16409  gcdcllem3  16430  bezout  16472  eulerth  16712  odzval  16721  pcprecl  16769  pcprendvds  16770  pcpremul  16773  pceulem  16775  prmreclem1  16846  prmreclem5  16850  prmreclem6  16851  4sqlem19  16893  vdwnn  16928  hashbcval  16932  gsumvalx  18568  symgfixelq  19330  efgsdm  19627  efgsfo  19636  ablfaclem3  19986  ltbwe  21967  coe1mul2lem2  22170  smadiadetlem3  22571  pptbas  22911  conncompss  23336  ptcmplem5  23959  ustuqtop  24150  utopsnneip  24152  icccmplem2  24728  minveclem5  25349  ivth  25371  ovolicc2lem5  25438  ovolicc  25440  opnmbllem  25518  vitali  25530  itg2monolem3  25669  elqaa  26246  radcnvle  26345  pserdvlem2  26354  lgamgulmlem5  26959  lgamcvglem  26966  wilth  26997  ftalem6  27004  precsexlemcbv  28131  bdayon  28196  ttgval  28838  axcontlem11  28937  lfgredgge2  29087  usgredgleordALT  29197  nbusgrf1o  29334  cusgrexg  29407  cusgrfilem2  29420  cusgrfi  29422  vtxdushgrfvedglem  29453  vtxdushgrfvedg  29454  vtxdginducedm1  29507  finsumvtxdg2sstep  29513  wwlksnextbij  29865  rusgrnumwwlks  29937  clwlkclwwlkfolem  29969  clwlkclwwlken  29974  clwwlknscsh  30024  hashecclwwlkn1  30039  umgrhashecclwwlk  30040  clwlknf1oclwwlknlem2  30044  clwlknf1oclwwlkn  30046  frgrwopreglem5lem  30282  frgrregorufr0  30286  fusgreghash2wsp  30300  dlwwlknondlwlknonf1o  30327  ubthlem3  30834  htth  30880  fcobijfs  32679  elrgspnsubrunlem1  33200  elrgspnsubrun  33202  1arithufd  33498  constrsuc  33707  constrcbvlem  33724  locfinreflem  33809  zarmxt1  33849  zarcmp  33851  ordtconnlem1  33893  dynkin  34136  ddemeas  34205  oddpwdc  34324  eulerpartgbij  34342  eulerpartlemn  34351  eulerpart  34352  ballotlemelo  34458  ballotleme  34467  ballotlem7  34506  reprsuc  34585  hgt750lema  34627  hgt750leme  34628  onvf1odlem3  35080  subfacp1lem6  35160  erdsze  35177  cvmscbv  35233  cvmsiota  35252  cvmlift2lem13  35290  satfv1  35338  neibastop2  36337  weiunfrlem  36440  topdifinffin  37324  poimirlem27  37629  mblfinlem1  37639  mblfinlem2  37640  lclkrs2  41522  aks4d1  42065  sticksstones2  42123  eldioph4i  42788  rfovcnvf1od  43980  fsovrfovd  43985  fsovcnvlem  43989  nzss  44293  supminfxr2  45452  limcperiod  45613  cncfshiftioo  45877  ioodvbdlimc1lem2  45917  ioodvbdlimc2lem  45919  dvnprodlem1  45931  dvnprod  45934  itgiccshift  45965  itgperiod  45966  stoweidlem49  46034  fourierdlem41  46133  fourierdlem48  46139  fourierdlem49  46140  fourierdlem54  46145  fourierdlem65  46156  fourierdlem70  46161  fourierdlem71  46162  fourierdlem81  46172  fourierdlem89  46180  fourierdlem90  46181  fourierdlem91  46182  fourierdlem92  46183  fourierdlem96  46187  fourierdlem97  46188  fourierdlem98  46189  fourierdlem99  46190  fourierdlem100  46191  fourierdlem103  46194  fourierdlem104  46195  fourierdlem105  46196  fourierdlem108  46199  fourierdlem109  46200  fourierdlem110  46201  fourierdlem112  46203  fourierdlem113  46204  elaa2  46219  etransclem11  46230  etransc  46268  salexct  46319  subsaliuncl  46343  sge0fodjrnlem  46401  meadjiun  46451  ovnsubadd  46557  hoidmv1le  46579  hoidmvlelem3  46582  hoidmvlelem5  46584  ovnhoi  46588  hspmbllem3  46613  hspmbl  46614  opnvonmbl  46619  ovolval4lem2  46635  ovolval5lem2  46638  ovolval5lem3  46639  ovolval5  46640  ovnovol  46644  issmf  46713  incsmf  46727  issmfle  46730  issmfgt  46741  smfadd  46750  decsmf  46752  issmfge  46755  smflimlem4  46759  smflim  46762  smfmul  46780  smflimsuplem2  46806  smflimsuplem5  46809  smflimsuplem7  46811  requad2  47611  uspgrlimlem1  47976  grlimedgclnbgr  47983  grlimgrtri  47991  gpgusgralem  48044  intubeu  48972  unilbeu  48973