Theorem cbvrabv 3442

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 2154 and ax-13 2371. (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 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2805	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3433	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3433	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2770	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  {cab 2709  {crab 3432

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433

This theorem is referenced by:  rabrabiOLD  3456  rru  3775  knatar  7356  oeeulem  8603  cofon1  8673  ordtypecbv  9514  ordtypelem9  9523  inf3lema  9621  oemapso  9679  oemapvali  9681  tz9.12lem3  9786  cofsmo  10266  enfin2i  10318  fin23lem33  10342  isf32lem11  10360  zorn2g  10500  pwfseqlem1  10655  pwfseqlem3  10657  zsupss  12923  zmin  12930  rpnnen1  12969  hashbc  14414  wrd2f1tovbij  14913  01sqrexlem7  15197  divalglem5  16342  bitsfzolem  16377  smupp1  16423  gcdcllem3  16444  bezout  16487  eulerth  16718  odzval  16726  pcprecl  16774  pcprendvds  16775  pcpremul  16778  pceulem  16780  prmreclem1  16851  prmreclem5  16855  prmreclem6  16856  4sqlem19  16898  vdwnn  16933  hashbcval  16937  gsumvalx  18597  symgfixelq  19303  efgsdm  19600  efgsfo  19609  ablfaclem3  19959  ltbwe  21605  coe1mul2lem2  21797  smadiadetlem3  22177  pptbas  22518  conncompss  22944  ptcmplem5  23567  ustuqtop  23758  utopsnneip  23760  icccmplem2  24346  minveclem5  24957  ivth  24978  ovolicc2lem5  25045  ovolicc  25047  opnmbllem  25125  vitali  25137  itg2monolem3  25277  elqaa  25842  radcnvle  25939  pserdvlem2  25947  lgamgulmlem5  26544  lgamcvglem  26551  wilth  26582  ftalem6  26589  precsexlemcbv  27662  ttgval  28164  ttgvalOLD  28165  axcontlem11  28270  lfgredgge2  28422  usgredgleordALT  28529  nbusgrf1o  28666  cusgrexg  28739  cusgrfilem2  28751  cusgrfi  28753  vtxdushgrfvedglem  28784  vtxdushgrfvedg  28785  vtxdginducedm1  28838  finsumvtxdg2sstep  28844  wwlksnextbij  29194  rusgrnumwwlks  29266  clwlkclwwlkfolem  29298  clwlkclwwlken  29303  clwwlknscsh  29353  hashecclwwlkn1  29368  umgrhashecclwwlk  29369  clwlknf1oclwwlknlem2  29373  clwlknf1oclwwlkn  29375  frgrwopreglem5lem  29611  frgrregorufr0  29615  fusgreghash2wsp  29629  dlwwlknondlwlknonf1o  29656  ubthlem3  30163  htth  30209  fcobijfs  31986  locfinreflem  32889  zarmxt1  32929  zarcmp  32931  ordtconnlem1  32973  dynkin  33234  ddemeas  33303  oddpwdc  33422  eulerpartgbij  33440  eulerpartlemn  33449  eulerpart  33450  ballotlemelo  33555  ballotleme  33564  ballotlem7  33603  reprsuc  33696  hgt750lema  33738  hgt750leme  33739  subfacp1lem6  34245  erdsze  34262  cvmscbv  34318  cvmsiota  34337  cvmlift2lem13  34375  satfv1  34423  neibastop2  35332  topdifinffin  36315  poimirlem27  36601  mblfinlem1  36611  mblfinlem2  36612  lclkrs2  40497  aks4d1  41040  sticksstones2  41049  eldioph4i  41632  rfovcnvf1od  42837  fsovrfovd  42842  fsovcnvlem  42846  nzss  43158  supminfxr2  44258  limcperiod  44423  cncfshiftioo  44687  ioodvbdlimc1lem2  44727  ioodvbdlimc2lem  44729  dvnprodlem1  44741  dvnprod  44744  itgiccshift  44775  itgperiod  44776  stoweidlem49  44844  fourierdlem41  44943  fourierdlem48  44949  fourierdlem49  44950  fourierdlem54  44955  fourierdlem65  44966  fourierdlem70  44971  fourierdlem71  44972  fourierdlem81  44982  fourierdlem89  44990  fourierdlem90  44991  fourierdlem91  44992  fourierdlem92  44993  fourierdlem96  44997  fourierdlem97  44998  fourierdlem98  44999  fourierdlem99  45000  fourierdlem100  45001  fourierdlem103  45004  fourierdlem104  45005  fourierdlem105  45006  fourierdlem108  45009  fourierdlem109  45010  fourierdlem110  45011  fourierdlem112  45013  fourierdlem113  45014  elaa2  45029  etransclem11  45040  etransc  45078  salexct  45129  subsaliuncl  45153  sge0fodjrnlem  45211  meadjiun  45261  ovnsubadd  45367  hoidmv1le  45389  hoidmvlelem3  45392  hoidmvlelem5  45394  ovnhoi  45398  hspmbllem3  45423  hspmbl  45424  opnvonmbl  45429  ovolval4lem2  45445  ovolval5lem2  45448  ovolval5lem3  45449  ovolval5  45450  ovnovol  45454  issmf  45523  incsmf  45537  issmfle  45540  issmfgt  45551  smfadd  45560  decsmf  45562  issmfge  45565  smflimlem4  45569  smflim  45572  smfmul  45590  smflimsuplem2  45616  smflimsuplem5  45619  smflimsuplem7  45621  requad2  46370  intubeu  47687  unilbeu  47688