Theorem cbvrabv 3406

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 2374. (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 2816	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2803	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3397	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3397	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2766	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

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

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 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397

This theorem is referenced by:  rru  3734  knatar  7300  oeeulem  8525  cofon1  8596  ordtypecbv  9414  ordtypelem9  9423  inf3lema  9525  oemapso  9583  oemapvali  9585  tz9.12lem3  9693  cofsmo  10171  enfin2i  10223  fin23lem33  10247  isf32lem11  10265  zorn2g  10405  pwfseqlem1  10560  pwfseqlem3  10562  zsupss  12841  zmin  12848  rpnnen1  12887  hashbc  14367  wrd2f1tovbij  14874  01sqrexlem7  15162  divalglem5  16315  bitsfzolem  16352  smupp1  16398  gcdcllem3  16419  bezout  16461  eulerth  16701  odzval  16710  pcprecl  16758  pcprendvds  16759  pcpremul  16762  pceulem  16764  prmreclem1  16835  prmreclem5  16839  prmreclem6  16840  4sqlem19  16882  vdwnn  16917  hashbcval  16921  gsumvalx  18592  symgfixelq  19353  efgsdm  19650  efgsfo  19659  ablfaclem3  20009  ltbwe  21990  coe1mul2lem2  22201  smadiadetlem3  22603  pptbas  22943  conncompss  23368  ptcmplem5  23991  ustuqtop  24181  utopsnneip  24183  icccmplem2  24759  minveclem5  25380  ivth  25402  ovolicc2lem5  25469  ovolicc  25471  opnmbllem  25549  vitali  25561  itg2monolem3  25700  elqaa  26277  radcnvle  26376  pserdvlem2  26385  lgamgulmlem5  26990  lgamcvglem  26997  wilth  27028  ftalem6  27035  precsexlemcbv  28164  bdayon  28229  ttgval  28873  axcontlem11  28973  lfgredgge2  29123  usgredgleordALT  29233  nbusgrf1o  29370  cusgrexg  29443  cusgrfilem2  29456  cusgrfi  29458  vtxdushgrfvedglem  29489  vtxdushgrfvedg  29490  vtxdginducedm1  29543  finsumvtxdg2sstep  29549  wwlksnextbij  29901  rusgrnumwwlks  29976  clwlkclwwlkfolem  30008  clwlkclwwlken  30013  clwwlknscsh  30063  hashecclwwlkn1  30078  umgrhashecclwwlk  30079  clwlknf1oclwwlknlem2  30083  clwlknf1oclwwlkn  30085  frgrwopreglem5lem  30321  frgrregorufr0  30325  fusgreghash2wsp  30339  dlwwlknondlwlknonf1o  30366  ubthlem3  30873  htth  30919  fcobijfs  32728  fcobijfs2  32729  elrgspnsubrunlem1  33257  elrgspnsubrun  33259  1arithufd  33557  extvfvcl  33629  mplvrpmfgalem  33637  constrsuc  33823  constrcbvlem  33840  locfinreflem  33925  zarmxt1  33965  zarcmp  33967  ordtconnlem1  34009  dynkin  34252  ddemeas  34321  oddpwdc  34439  eulerpartgbij  34457  eulerpartlemn  34466  eulerpart  34467  ballotlemelo  34573  ballotleme  34582  ballotlem7  34621  reprsuc  34700  hgt750lema  34742  hgt750leme  34743  fineqvnttrclse  35216  onvf1odlem3  35221  subfacp1lem6  35301  erdsze  35318  cvmscbv  35374  cvmsiota  35393  cvmlift2lem13  35431  satfv1  35479  neibastop2  36477  weiunfrlem  36580  topdifinffin  37465  poimirlem27  37760  mblfinlem1  37770  mblfinlem2  37771  lclkrs2  41712  aks4d1  42255  sticksstones2  42313  eldioph4i  42969  rfovcnvf1od  44161  fsovrfovd  44166  fsovcnvlem  44170  nzss  44474  supminfxr2  45629  limcperiod  45790  cncfshiftioo  46052  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  dvnprodlem1  46106  dvnprod  46109  itgiccshift  46140  itgperiod  46141  stoweidlem49  46209  fourierdlem41  46308  fourierdlem48  46314  fourierdlem49  46315  fourierdlem54  46320  fourierdlem65  46331  fourierdlem70  46336  fourierdlem71  46337  fourierdlem81  46347  fourierdlem89  46355  fourierdlem90  46356  fourierdlem91  46357  fourierdlem92  46358  fourierdlem96  46362  fourierdlem97  46363  fourierdlem98  46364  fourierdlem99  46365  fourierdlem100  46366  fourierdlem103  46369  fourierdlem104  46370  fourierdlem105  46371  fourierdlem108  46374  fourierdlem109  46375  fourierdlem110  46376  fourierdlem112  46378  fourierdlem113  46379  elaa2  46394  etransclem11  46405  etransc  46443  salexct  46494  subsaliuncl  46518  sge0fodjrnlem  46576  meadjiun  46626  ovnsubadd  46732  hoidmv1le  46754  hoidmvlelem3  46757  hoidmvlelem5  46759  ovnhoi  46763  hspmbllem3  46788  hspmbl  46789  opnvonmbl  46794  ovolval4lem2  46810  ovolval5lem2  46813  ovolval5lem3  46814  ovolval5  46815  ovnovol  46819  issmf  46888  incsmf  46902  issmfle  46905  issmfgt  46916  smfadd  46925  decsmf  46927  issmfge  46930  smflimlem4  46934  smflim  46937  smfmul  46955  smflimsuplem2  46981  smflimsuplem5  46984  smflimsuplem7  46986  requad2  47785  uspgrlimlem1  48150  grlimedgclnbgr  48157  grlimgrtri  48165  gpgusgralem  48218  intubeu  49145  unilbeu  49146