Theorem cbvrabv 3409

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 2162 and ax-13 2376. (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 2819	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2806	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3400	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3400	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2769	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113  {cab 2714  {crab 3399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400

This theorem is referenced by:  rru  3737  knatar  7303  oeeulem  8529  cofon1  8600  ordtypecbv  9422  ordtypelem9  9431  inf3lema  9533  oemapso  9591  oemapvali  9593  tz9.12lem3  9701  cofsmo  10179  enfin2i  10231  fin23lem33  10255  isf32lem11  10273  zorn2g  10413  pwfseqlem1  10569  pwfseqlem3  10571  zsupss  12850  zmin  12857  rpnnen1  12896  hashbc  14376  wrd2f1tovbij  14883  01sqrexlem7  15171  divalglem5  16324  bitsfzolem  16361  smupp1  16407  gcdcllem3  16428  bezout  16470  eulerth  16710  odzval  16719  pcprecl  16767  pcprendvds  16768  pcpremul  16771  pceulem  16773  prmreclem1  16844  prmreclem5  16848  prmreclem6  16849  4sqlem19  16891  vdwnn  16926  hashbcval  16930  gsumvalx  18601  symgfixelq  19362  efgsdm  19659  efgsfo  19668  ablfaclem3  20018  ltbwe  21999  coe1mul2lem2  22210  smadiadetlem3  22612  pptbas  22952  conncompss  23377  ptcmplem5  24000  ustuqtop  24190  utopsnneip  24192  icccmplem2  24768  minveclem5  25389  ivth  25411  ovolicc2lem5  25478  ovolicc  25480  opnmbllem  25558  vitali  25570  itg2monolem3  25709  elqaa  26286  radcnvle  26385  pserdvlem2  26394  lgamgulmlem5  26999  lgamcvglem  27006  wilth  27037  ftalem6  27044  precsexlemcbv  28202  bdayons  28272  ttgval  28947  axcontlem11  29047  lfgredgge2  29197  usgredgleordALT  29307  nbusgrf1o  29444  cusgrexg  29517  cusgrfilem2  29530  cusgrfi  29532  vtxdushgrfvedglem  29563  vtxdushgrfvedg  29564  vtxdginducedm1  29617  finsumvtxdg2sstep  29623  wwlksnextbij  29975  rusgrnumwwlks  30050  clwlkclwwlkfolem  30082  clwlkclwwlken  30087  clwwlknscsh  30137  hashecclwwlkn1  30152  umgrhashecclwwlk  30153  clwlknf1oclwwlknlem2  30157  clwlknf1oclwwlkn  30159  frgrwopreglem5lem  30395  frgrregorufr0  30399  fusgreghash2wsp  30413  dlwwlknondlwlknonf1o  30440  ubthlem3  30947  htth  30993  fcobijfs  32800  fcobijfs2  32801  elrgspnsubrunlem1  33329  elrgspnsubrun  33331  1arithufd  33629  extvfvcl  33701  mplvrpmfgalem  33709  constrsuc  33895  constrcbvlem  33912  locfinreflem  33997  zarmxt1  34037  zarcmp  34039  ordtconnlem1  34081  dynkin  34324  ddemeas  34393  oddpwdc  34511  eulerpartgbij  34529  eulerpartlemn  34538  eulerpart  34539  ballotlemelo  34645  ballotleme  34654  ballotlem7  34693  reprsuc  34772  hgt750lema  34814  hgt750leme  34815  fineqvnttrclse  35280  onvf1odlem3  35299  subfacp1lem6  35379  erdsze  35396  cvmscbv  35452  cvmsiota  35471  cvmlift2lem13  35509  satfv1  35557  neibastop2  36555  weiunfrlem  36658  topdifinffin  37553  poimirlem27  37848  mblfinlem1  37858  mblfinlem2  37859  lclkrs2  41800  aks4d1  42343  sticksstones2  42401  eldioph4i  43054  rfovcnvf1od  44245  fsovrfovd  44250  fsovcnvlem  44254  nzss  44558  supminfxr2  45713  limcperiod  45874  cncfshiftioo  46136  ioodvbdlimc1lem2  46176  ioodvbdlimc2lem  46178  dvnprodlem1  46190  dvnprod  46193  itgiccshift  46224  itgperiod  46225  stoweidlem49  46293  fourierdlem41  46392  fourierdlem48  46398  fourierdlem49  46399  fourierdlem54  46404  fourierdlem65  46415  fourierdlem70  46420  fourierdlem71  46421  fourierdlem81  46431  fourierdlem89  46439  fourierdlem90  46440  fourierdlem91  46441  fourierdlem92  46442  fourierdlem96  46446  fourierdlem97  46447  fourierdlem98  46448  fourierdlem99  46449  fourierdlem100  46450  fourierdlem103  46453  fourierdlem104  46454  fourierdlem105  46455  fourierdlem108  46458  fourierdlem109  46459  fourierdlem110  46460  fourierdlem112  46462  fourierdlem113  46463  elaa2  46478  etransclem11  46489  etransc  46527  salexct  46578  subsaliuncl  46602  sge0fodjrnlem  46660  meadjiun  46710  ovnsubadd  46816  hoidmv1le  46838  hoidmvlelem3  46841  hoidmvlelem5  46843  ovnhoi  46847  hspmbllem3  46872  hspmbl  46873  opnvonmbl  46878  ovolval4lem2  46894  ovolval5lem2  46897  ovolval5lem3  46898  ovolval5  46899  ovnovol  46903  issmf  46972  incsmf  46986  issmfle  46989  issmfgt  47000  smfadd  47009  decsmf  47011  issmfge  47014  smflimlem4  47018  smflim  47021  smfmul  47039  smflimsuplem2  47065  smflimsuplem5  47068  smflimsuplem7  47070  requad2  47869  uspgrlimlem1  48234  grlimedgclnbgr  48241  grlimgrtri  48249  gpgusgralem  48302  intubeu  49229  unilbeu  49230