Theorem cbvrabv 3454

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 2380. (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 2827	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2815	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3444	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3444	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2778	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2108  {cab 2717  {crab 3443

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444

This theorem is referenced by:  rabrabiOLD  3469  rru  3801  knatar  7393  oeeulem  8657  cofon1  8728  ordtypecbv  9586  ordtypelem9  9595  inf3lema  9693  oemapso  9751  oemapvali  9753  tz9.12lem3  9858  cofsmo  10338  enfin2i  10390  fin23lem33  10414  isf32lem11  10432  zorn2g  10572  pwfseqlem1  10727  pwfseqlem3  10729  zsupss  13002  zmin  13009  rpnnen1  13048  hashbc  14502  wrd2f1tovbij  15009  01sqrexlem7  15297  divalglem5  16445  bitsfzolem  16480  smupp1  16526  gcdcllem3  16547  bezout  16590  eulerth  16830  odzval  16838  pcprecl  16886  pcprendvds  16887  pcpremul  16890  pceulem  16892  prmreclem1  16963  prmreclem5  16967  prmreclem6  16968  4sqlem19  17010  vdwnn  17045  hashbcval  17049  gsumvalx  18714  symgfixelq  19475  efgsdm  19772  efgsfo  19781  ablfaclem3  20131  ltbwe  22085  coe1mul2lem2  22292  smadiadetlem3  22695  pptbas  23036  conncompss  23462  ptcmplem5  24085  ustuqtop  24276  utopsnneip  24278  icccmplem2  24864  minveclem5  25486  ivth  25508  ovolicc2lem5  25575  ovolicc  25577  opnmbllem  25655  vitali  25667  itg2monolem3  25807  elqaa  26382  radcnvle  26481  pserdvlem2  26490  lgamgulmlem5  27094  lgamcvglem  27101  wilth  27132  ftalem6  27139  precsexlemcbv  28248  ttgval  28901  ttgvalOLD  28902  axcontlem11  29007  lfgredgge2  29159  usgredgleordALT  29269  nbusgrf1o  29406  cusgrexg  29479  cusgrfilem2  29492  cusgrfi  29494  vtxdushgrfvedglem  29525  vtxdushgrfvedg  29526  vtxdginducedm1  29579  finsumvtxdg2sstep  29585  wwlksnextbij  29935  rusgrnumwwlks  30007  clwlkclwwlkfolem  30039  clwlkclwwlken  30044  clwwlknscsh  30094  hashecclwwlkn1  30109  umgrhashecclwwlk  30110  clwlknf1oclwwlknlem2  30114  clwlknf1oclwwlkn  30116  frgrwopreglem5lem  30352  frgrregorufr0  30356  fusgreghash2wsp  30370  dlwwlknondlwlknonf1o  30397  ubthlem3  30904  htth  30950  fcobijfs  32737  1arithufd  33541  constrsuc  33728  locfinreflem  33786  zarmxt1  33826  zarcmp  33828  ordtconnlem1  33870  dynkin  34131  ddemeas  34200  oddpwdc  34319  eulerpartgbij  34337  eulerpartlemn  34346  eulerpart  34347  ballotlemelo  34452  ballotleme  34461  ballotlem7  34500  reprsuc  34592  hgt750lema  34634  hgt750leme  34635  subfacp1lem6  35153  erdsze  35170  cvmscbv  35226  cvmsiota  35245  cvmlift2lem13  35283  satfv1  35331  neibastop2  36327  weiunfrlem  36430  topdifinffin  37314  poimirlem27  37607  mblfinlem1  37617  mblfinlem2  37618  lclkrs2  41497  aks4d1  42046  sticksstones2  42104  eldioph4i  42768  rfovcnvf1od  43966  fsovrfovd  43971  fsovcnvlem  43975  nzss  44286  supminfxr2  45384  limcperiod  45549  cncfshiftioo  45813  ioodvbdlimc1lem2  45853  ioodvbdlimc2lem  45855  dvnprodlem1  45867  dvnprod  45870  itgiccshift  45901  itgperiod  45902  stoweidlem49  45970  fourierdlem41  46069  fourierdlem48  46075  fourierdlem49  46076  fourierdlem54  46081  fourierdlem65  46092  fourierdlem70  46097  fourierdlem71  46098  fourierdlem81  46108  fourierdlem89  46116  fourierdlem90  46117  fourierdlem91  46118  fourierdlem92  46119  fourierdlem96  46123  fourierdlem97  46124  fourierdlem98  46125  fourierdlem99  46126  fourierdlem100  46127  fourierdlem103  46130  fourierdlem104  46131  fourierdlem105  46132  fourierdlem108  46135  fourierdlem109  46136  fourierdlem110  46137  fourierdlem112  46139  fourierdlem113  46140  elaa2  46155  etransclem11  46166  etransc  46204  salexct  46255  subsaliuncl  46279  sge0fodjrnlem  46337  meadjiun  46387  ovnsubadd  46493  hoidmv1le  46515  hoidmvlelem3  46518  hoidmvlelem5  46520  ovnhoi  46524  hspmbllem3  46549  hspmbl  46550  opnvonmbl  46555  ovolval4lem2  46571  ovolval5lem2  46574  ovolval5lem3  46575  ovolval5  46576  ovnovol  46580  issmf  46649  incsmf  46663  issmfle  46666  issmfgt  46677  smfadd  46686  decsmf  46688  issmfge  46691  smflimlem4  46695  smflim  46698  smfmul  46716  smflimsuplem2  46742  smflimsuplem5  46745  smflimsuplem7  46747  requad2  47497  uspgrlimlem1  47812  grlimgrtri  47820  intubeu  48656  unilbeu  48657