Theorem cbvrabv 3447

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 2157 and ax-13 2377. (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 2824	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2812	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3437	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3437	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2775	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2108  {cab 2714  {crab 3436

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437

This theorem is referenced by:  rru  3785  knatar  7377  oeeulem  8639  cofon1  8710  ordtypecbv  9557  ordtypelem9  9566  inf3lema  9664  oemapso  9722  oemapvali  9724  tz9.12lem3  9829  cofsmo  10309  enfin2i  10361  fin23lem33  10385  isf32lem11  10403  zorn2g  10543  pwfseqlem1  10698  pwfseqlem3  10700  zsupss  12979  zmin  12986  rpnnen1  13025  hashbc  14492  wrd2f1tovbij  14999  01sqrexlem7  15287  divalglem5  16434  bitsfzolem  16471  smupp1  16517  gcdcllem3  16538  bezout  16580  eulerth  16820  odzval  16829  pcprecl  16877  pcprendvds  16878  pcpremul  16881  pceulem  16883  prmreclem1  16954  prmreclem5  16958  prmreclem6  16959  4sqlem19  17001  vdwnn  17036  hashbcval  17040  gsumvalx  18689  symgfixelq  19451  efgsdm  19748  efgsfo  19757  ablfaclem3  20107  ltbwe  22062  coe1mul2lem2  22271  smadiadetlem3  22674  pptbas  23015  conncompss  23441  ptcmplem5  24064  ustuqtop  24255  utopsnneip  24257  icccmplem2  24845  minveclem5  25467  ivth  25489  ovolicc2lem5  25556  ovolicc  25558  opnmbllem  25636  vitali  25648  itg2monolem3  25787  elqaa  26364  radcnvle  26463  pserdvlem2  26472  lgamgulmlem5  27076  lgamcvglem  27083  wilth  27114  ftalem6  27121  precsexlemcbv  28230  ttgval  28883  ttgvalOLD  28884  axcontlem11  28989  lfgredgge2  29141  usgredgleordALT  29251  nbusgrf1o  29388  cusgrexg  29461  cusgrfilem2  29474  cusgrfi  29476  vtxdushgrfvedglem  29507  vtxdushgrfvedg  29508  vtxdginducedm1  29561  finsumvtxdg2sstep  29567  wwlksnextbij  29922  rusgrnumwwlks  29994  clwlkclwwlkfolem  30026  clwlkclwwlken  30031  clwwlknscsh  30081  hashecclwwlkn1  30096  umgrhashecclwwlk  30097  clwlknf1oclwwlknlem2  30101  clwlknf1oclwwlkn  30103  frgrwopreglem5lem  30339  frgrregorufr0  30343  fusgreghash2wsp  30357  dlwwlknondlwlknonf1o  30384  ubthlem3  30891  htth  30937  fcobijfs  32734  elrgspnsubrunlem1  33251  elrgspnsubrun  33253  1arithufd  33576  constrsuc  33779  locfinreflem  33839  zarmxt1  33879  zarcmp  33881  ordtconnlem1  33923  dynkin  34168  ddemeas  34237  oddpwdc  34356  eulerpartgbij  34374  eulerpartlemn  34383  eulerpart  34384  ballotlemelo  34490  ballotleme  34499  ballotlem7  34538  reprsuc  34630  hgt750lema  34672  hgt750leme  34673  subfacp1lem6  35190  erdsze  35207  cvmscbv  35263  cvmsiota  35282  cvmlift2lem13  35320  satfv1  35368  neibastop2  36362  weiunfrlem  36465  topdifinffin  37349  poimirlem27  37654  mblfinlem1  37664  mblfinlem2  37665  lclkrs2  41542  aks4d1  42090  sticksstones2  42148  eldioph4i  42823  rfovcnvf1od  44017  fsovrfovd  44022  fsovcnvlem  44026  nzss  44336  supminfxr2  45480  limcperiod  45643  cncfshiftioo  45907  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  dvnprodlem1  45961  dvnprod  45964  itgiccshift  45995  itgperiod  45996  stoweidlem49  46064  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem54  46175  fourierdlem65  46186  fourierdlem70  46191  fourierdlem71  46192  fourierdlem81  46202  fourierdlem89  46210  fourierdlem90  46211  fourierdlem91  46212  fourierdlem92  46213  fourierdlem96  46217  fourierdlem97  46218  fourierdlem98  46219  fourierdlem99  46220  fourierdlem100  46221  fourierdlem103  46224  fourierdlem104  46225  fourierdlem105  46226  fourierdlem108  46229  fourierdlem109  46230  fourierdlem110  46231  fourierdlem112  46233  fourierdlem113  46234  elaa2  46249  etransclem11  46260  etransc  46298  salexct  46349  subsaliuncl  46373  sge0fodjrnlem  46431  meadjiun  46481  ovnsubadd  46587  hoidmv1le  46609  hoidmvlelem3  46612  hoidmvlelem5  46614  ovnhoi  46618  hspmbllem3  46643  hspmbl  46644  opnvonmbl  46649  ovolval4lem2  46665  ovolval5lem2  46668  ovolval5lem3  46669  ovolval5  46670  ovnovol  46674  issmf  46743  incsmf  46757  issmfle  46760  issmfgt  46771  smfadd  46780  decsmf  46782  issmfge  46785  smflimlem4  46789  smflim  46792  smfmul  46810  smflimsuplem2  46836  smflimsuplem5  46839  smflimsuplem7  46841  requad2  47610  uspgrlimlem1  47955  grlimgrtri  47963  gpgusgralem  48011  intubeu  48873  unilbeu  48874