Theorem cbvrabv 3402

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 2168 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 2823	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 638	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2810	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3393	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3393	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2773	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   = wceq 1547   ∈ wcel 2119  {cab 2718  {crab 3392

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393

This theorem is referenced by:  rru  3727  knatar  7308  oeeulem  8534  cofon1  8605  ordtypecbv  9429  ordtypelem9  9438  inf3lema  9543  oemapso  9601  oemapvali  9603  tz9.12lem3  9711  cofsmo  10189  enfin2i  10241  fin23lem33  10265  isf32lem11  10283  zorn2g  10423  pwfseqlem1  10579  pwfseqlem3  10581  zsupss  12885  zmin  12892  rpnnen1  12931  hashbc  14413  wrd2f1tovbij  14920  01sqrexlem7  15208  divalglem5  16364  bitsfzolem  16401  smupp1  16447  gcdcllem3  16468  bezout  16510  eulerth  16751  odzval  16760  pcprecl  16808  pcprendvds  16809  pcpremul  16812  pceulem  16814  prmreclem1  16885  prmreclem5  16889  prmreclem6  16890  4sqlem19  16932  vdwnn  16967  hashbcval  16971  gsumvalx  18642  symgfixelq  19406  efgsdm  19703  efgsfo  19712  ablfaclem3  20062  ltbwe  22027  coe1mul2lem2  22261  smadiadetlem3  22658  pptbas  22998  conncompss  23423  ptcmplem5  24046  ustuqtop  24236  utopsnneip  24238  icccmplem2  24814  minveclem5  25425  ivth  25446  ovolicc2lem5  25513  ovolicc  25515  opnmbllem  25593  vitali  25605  itg2monolem3  25744  elqaa  26313  radcnvle  26410  pserdvlem2  26418  lgamgulmlem5  27021  lgamcvglem  27028  wilth  27059  ftalem6  27066  precsexlemcbv  28223  bdayons  28293  ttgval  28968  axcontlem11  29068  lfgredgge2  29218  usgredgleordALT  29328  nbusgrf1o  29465  cusgrexg  29538  cusgrfilem2  29550  cusgrfi  29552  vtxdushgrfvedglem  29583  vtxdushgrfvedg  29584  vtxdginducedm1  29637  finsumvtxdg2sstep  29643  wwlksnextbij  29995  rusgrnumwwlks  30070  clwlkclwwlkfolem  30102  clwlkclwwlken  30107  clwwlknscsh  30157  hashecclwwlkn1  30172  umgrhashecclwwlk  30173  clwlknf1oclwwlknlem2  30177  clwlknf1oclwwlkn  30179  frgrwopreglem5lem  30415  frgrregorufr0  30419  fusgreghash2wsp  30433  dlwwlknondlwlknonf1o  30460  ubthlem3  30968  htth  31014  fcobijfs  32820  fcobijfs2  32821  elrgspnsubrunlem1  33335  elrgspnsubrun  33337  1arithufd  33638  extvfvcl  33727  mplvrpmfgalem  33735  constrsuc  33929  constrcbvlem  33946  locfinreflem  34031  zarmxt1  34071  zarcmp  34073  ordtconnlem1  34115  dynkin  34358  ddemeas  34427  oddpwdc  34545  eulerpartgbij  34563  eulerpartlemn  34572  eulerpart  34573  ballotlemelo  34679  ballotleme  34688  ballotlem7  34727  reprsuc  34806  hgt750lema  34848  hgt750leme  34849  fineqvnttrclse  35312  onvf1odlem3  35340  subfacp1lem6  35420  erdsze  35437  cvmscbv  35493  cvmsiota  35512  cvmlift2lem13  35550  satfv1  35598  neibastop2  36596  weiunfrlem  36699  topdifinffin  37717  poimirlem27  38021  mblfinlem1  38031  mblfinlem2  38032  lclkrs2  42039  aks4d1  42581  sticksstones2  42639  eldioph4i  43264  rfovcnvf1od  44455  fsovrfovd  44460  fsovcnvlem  44464  nzss  44768  supminfxr2  45919  limcperiod  46080  cncfshiftioo  46342  ioodvbdlimc1lem2  46382  ioodvbdlimc2lem  46384  dvnprodlem1  46396  dvnprod  46399  itgiccshift  46430  itgperiod  46431  stoweidlem49  46499  fourierdlem41  46598  fourierdlem48  46604  fourierdlem49  46605  fourierdlem54  46610  fourierdlem65  46621  fourierdlem70  46626  fourierdlem71  46627  fourierdlem81  46637  fourierdlem89  46645  fourierdlem90  46646  fourierdlem91  46647  fourierdlem92  46648  fourierdlem96  46652  fourierdlem97  46653  fourierdlem98  46654  fourierdlem99  46655  fourierdlem100  46656  fourierdlem103  46659  fourierdlem104  46660  fourierdlem105  46661  fourierdlem108  46664  fourierdlem109  46665  fourierdlem110  46666  fourierdlem112  46668  fourierdlem113  46669  elaa2  46684  etransclem11  46695  etransc  46733  salexct  46784  subsaliuncl  46808  sge0fodjrnlem  46866  meadjiun  46916  ovnsubadd  47022  hoidmv1le  47044  hoidmvlelem3  47047  hoidmvlelem5  47049  ovnhoi  47053  hspmbllem3  47078  hspmbl  47079  opnvonmbl  47084  ovolval4lem2  47100  ovolval5lem2  47103  ovolval5lem3  47104  ovolval5  47105  ovnovol  47109  issmf  47178  incsmf  47192  issmfle  47195  issmfgt  47206  smfadd  47215  decsmf  47217  issmfge  47220  smflimlem4  47224  smflim  47227  smfmul  47245  smflimsuplem2  47271  smflimsuplem5  47274  smflimsuplem7  47276  requad2  48121  uspgrlimlem1  48486  grlimedgclnbgr  48493  grlimgrtri  48501  gpgusgralem  48554  intubeu  49481  unilbeu  49482