Theorem cbvrabv 3426

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 2197 and ax-13 2404. (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 2847	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2834	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3417	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3417	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2796	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401   = wceq 1570   ∈ wcel 2147  {cab 2741  {crab 3416

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417

This theorem is used by:  rur  3740  knatar  7396  oeeulem  8646  cofon1  8717  ordtypecbv  9546  ordtypelem9  9555  inf3lema  9660  oemapso  9718  oemapvali  9720  tz9.12lem3  9831  cardprcALT  10098  cofsmo  10384  enfin2i  10436  fin23lem33  10460  isf32lem11  10478  zorn2g  10618  pwfseqlem1  10780  pwfseqlem3  10782  zsupss  13102  zmin  13109  rpnnen1  13149  hashbc  14637  wrd2f1tovbij  15154  01sqrexlem7  15456  divalglem5  16608  bitsfzolem  16645  smupp1  16691  gcdcllem3  16712  bezout  16757  eulerth  17001  odzval  17010  pcprecl  17058  pcprendvds  17059  pcpremul  17062  pceulem  17064  prmreclem1  17135  prmreclem5  17139  prmreclem6  17140  4sqlem19  17182  vdwnn  17217  hashbcval  17221  gsumvalx  18906  symgfixelq  19689  efgsdm  19986  efgsfo  19995  ablfaclem3  20345  ltbwe  22397  coe1mul2lem2  22631  smadiadetlem3  23027  pptbas  23370  conncompss  23795  ptcmplem5  24419  ustuqtop  24609  utopsnneip  24611  icccmplem2  25187  minveclem5  25798  ivth  25819  ovolicc2lem5  25886  ovolicc  25888  opnmbllem  25966  vitali  25978  itg2monolem3  26117  elqaa  26691  radcnvle  26793  pserdvlem2  26801  lgamgulmlem5  27406  lgamcvglem  27413  wilth  27444  ftalem6  27451  precsexlemcbv  28638  bdayons  28708  ttgval  29498  axcontlem11  29598  lfgredgge2  29748  usgredgleordALT  29861  nbusgrf1o  29998  cusgrexg  30071  cusgrfilem2  30083  cusgrfi  30085  vtxdushgrfvedglem  30116  vtxdushgrfvedg  30117  vtxdginducedm1  30170  finsumvtxdg2sstep  30176  wwlksnextbij  30537  rusgrnumwwlks  30612  clwlkclwwlkfolem  30644  clwlkclwwlken  30649  clwwlknscsh  30699  hashecclwwlkn1  30714  umgrhashecclwwlk  30715  clwlknf1oclwwlknlem2  30719  clwlknf1oclwwlkn  30721  frgrwopreglem5lem  30967  frgrregorufr0  30971  fusgreghash2wsp  30985  dlwwlknondlwlknonf1o  31012  ubthlem3  31520  htth  31566  fcobijfs  33399  fcobijfs2  33400  elrgspnsubrunlem1  33897  elrgspnsubrun  33899  1arithufd  34177  extvfvcl  34272  mplvrpmfgalem  34280  constrsuc  34474  constrcbvlem  34491  locfinreflem  34576  zarmxt1  34616  zarcmp  34618  ordtconnlem1  34660  dynkin  34904  ddemeas  34973  oddpwdc  35090  eulerpartgbij  35108  eulerpartlemn  35117  eulerpart  35118  ballotlemelo  35224  ballotleme  35233  ballotlem7  35272  reprsuc  35348  hgt750lema  35390  hgt750leme  35391  werankwe  35855  werankwe2  35856  fineqvnttrclse  35926  onvf1odlem3  36067  subfacp1lem6  36151  erdsze  36168  cvmscbv  36224  cvmsiota  36243  cvmlift2lem13  36281  satfv1  36329  neibastop2  37357  weiunfrlem  37460  topdifinffin  38532  poimirlem27  38826  mblfinlem1  38836  mblfinlem2  38837  lclkrs2  42856  aks4d1  43398  sticksstones2  43456  eldioph4i  44079  rfovcnvf1od  45259  fsovrfovd  45264  fsovcnvlem  45268  nzss  45556  supminfxr2  46746  limcperiod  46907  cncfshiftioo  47169  ioodvbdlimc1lem2  47209  ioodvbdlimc2lem  47211  dvnprodlem1  47223  dvnprod  47226  itgiccshift  47257  itgperiod  47258  stoweidlem49  47326  fourierdlem41  47425  fourierdlem48  47431  fourierdlem49  47432  fourierdlem54  47437  fourierdlem65  47448  fourierdlem70  47453  fourierdlem71  47454  fourierdlem81  47464  fourierdlem89  47472  fourierdlem90  47473  fourierdlem91  47474  fourierdlem92  47475  fourierdlem96  47479  fourierdlem97  47480  fourierdlem98  47481  fourierdlem99  47482  fourierdlem100  47483  fourierdlem103  47486  fourierdlem104  47487  fourierdlem105  47488  fourierdlem108  47491  fourierdlem109  47492  fourierdlem110  47493  fourierdlem112  47495  fourierdlem113  47496  elaa2  47511  etransclem11  47522  etransc  47560  salexct  47611  subsaliuncl  47635  sge0fodjrnlem  47693  meadjiun  47743  ovnsubadd  47849  hoidmv1le  47871  hoidmvlelem3  47874  hoidmvlelem5  47876  ovnhoi  47880  hspmbllem3  47905  hspmbl  47906  opnvonmbl  47911  ovolval4lem2  47927  ovolval5lem2  47930  ovolval5lem3  47931  ovolval5  47932  ovnovol  47936  issmf  48005  incsmf  48019  issmfle  48022  issmfgt  48033  smfadd  48042  decsmf  48044  issmfge  48047  smflimlem4  48051  smflim  48054  smfmul  48072  smflimsuplem2  48098  smflimsuplem5  48101  smflimsuplem7  48103  requad2  48988  uspgrlimlem1  49353  grlimedgclnbgr  49360  grlimgrtri  49368  gpgusgralem  49421  intubeu  50423  unilbeu  50424