Theorem cbvrabv 3433

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 2198 and ax-13 2410. (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 2852	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 643	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2839	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3424	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3424	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2802	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   = wceq 1567   ∈ wcel 2149  {cab 2747  {crab 3423

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424

This theorem is referenced by:  rru  3751  knatar  7353  oeeulem  8583  cofon1  8654  ordtypecbv  9475  ordtypelem9  9484  inf3lema  9589  oemapso  9647  oemapvali  9649  tz9.12lem3  9757  cofsmo  10249  enfin2i  10301  fin23lem33  10325  isf32lem11  10343  zorn2g  10483  pwfseqlem1  10639  pwfseqlem3  10641  zsupss  12957  zmin  12964  rpnnen1  13003  hashbc  14486  wrd2f1tovbij  14993  01sqrexlem7  15295  divalglem5  16451  bitsfzolem  16488  smupp1  16534  gcdcllem3  16555  bezout  16597  eulerth  16838  odzval  16847  pcprecl  16895  pcprendvds  16896  pcpremul  16899  pceulem  16901  prmreclem1  16972  prmreclem5  16976  prmreclem6  16977  4sqlem19  17019  vdwnn  17054  hashbcval  17058  gsumvalx  18730  symgfixelq  19499  efgsdm  19796  efgsfo  19805  ablfaclem3  20155  ltbwe  22160  coe1mul2lem2  22394  smadiadetlem3  22790  pptbas  23130  conncompss  23555  ptcmplem5  24178  ustuqtop  24368  utopsnneip  24370  icccmplem2  24946  minveclem5  25557  ivth  25578  ovolicc2lem5  25645  ovolicc  25647  opnmbllem  25725  vitali  25737  itg2monolem3  25876  elqaa  26448  radcnvle  26545  pserdvlem2  26553  lgamgulmlem5  27159  lgamcvglem  27166  wilth  27197  ftalem6  27204  precsexlemcbv  28361  bdayons  28431  ttgval  29161  axcontlem11  29261  lfgredgge2  29411  usgredgleordALT  29521  nbusgrf1o  29658  cusgrexg  29731  cusgrfilem2  29743  cusgrfi  29745  vtxdushgrfvedglem  29776  vtxdushgrfvedg  29777  vtxdginducedm1  29830  finsumvtxdg2sstep  29836  wwlksnextbij  30188  rusgrnumwwlks  30263  clwlkclwwlkfolem  30295  clwlkclwwlken  30300  clwwlknscsh  30350  hashecclwwlkn1  30365  umgrhashecclwwlk  30366  clwlknf1oclwwlknlem2  30370  clwlknf1oclwwlkn  30372  frgrwopreglem5lem  30608  frgrregorufr0  30612  fusgreghash2wsp  30626  dlwwlknondlwlknonf1o  30653  ubthlem3  31161  htth  31207  fcobijfs  33003  fcobijfs2  33004  elrgspnsubrunlem1  33504  elrgspnsubrun  33506  1arithufd  33779  extvfvcl  33867  mplvrpmfgalem  33875  constrsuc  34069  constrcbvlem  34086  locfinreflem  34171  zarmxt1  34211  zarcmp  34213  ordtconnlem1  34255  dynkin  34498  ddemeas  34567  oddpwdc  34685  eulerpartgbij  34703  eulerpartlemn  34712  eulerpart  34713  ballotlemelo  34819  ballotleme  34828  ballotlem7  34867  reprsuc  34943  hgt750lema  34985  hgt750leme  34986  fineqvnttrclse  35456  onvf1odlem3  35484  subfacp1lem6  35572  erdsze  35589  cvmscbv  35645  cvmsiota  35664  cvmlift2lem13  35702  satfv1  35750  neibastop2  36757  weiunfrlem  36860  topdifinffin  37877  poimirlem27  38181  mblfinlem1  38191  mblfinlem2  38192  lclkrs2  42199  aks4d1  42741  sticksstones2  42799  eldioph4i  43424  rfovcnvf1od  44615  fsovrfovd  44620  fsovcnvlem  44624  nzss  44912  supminfxr2  46068  limcperiod  46229  cncfshiftioo  46491  ioodvbdlimc1lem2  46531  ioodvbdlimc2lem  46533  dvnprodlem1  46545  dvnprod  46548  itgiccshift  46579  itgperiod  46580  stoweidlem49  46648  fourierdlem41  46747  fourierdlem48  46753  fourierdlem49  46754  fourierdlem54  46759  fourierdlem65  46770  fourierdlem70  46775  fourierdlem71  46776  fourierdlem81  46786  fourierdlem89  46794  fourierdlem90  46795  fourierdlem91  46796  fourierdlem92  46797  fourierdlem96  46801  fourierdlem97  46802  fourierdlem98  46803  fourierdlem99  46804  fourierdlem100  46805  fourierdlem103  46808  fourierdlem104  46809  fourierdlem105  46810  fourierdlem108  46813  fourierdlem109  46814  fourierdlem110  46815  fourierdlem112  46817  fourierdlem113  46818  elaa2  46833  etransclem11  46844  etransc  46882  salexct  46933  subsaliuncl  46957  sge0fodjrnlem  47015  meadjiun  47065  ovnsubadd  47171  hoidmv1le  47193  hoidmvlelem3  47196  hoidmvlelem5  47198  ovnhoi  47202  hspmbllem3  47227  hspmbl  47228  opnvonmbl  47233  ovolval4lem2  47249  ovolval5lem2  47252  ovolval5lem3  47253  ovolval5  47254  ovnovol  47258  issmf  47327  incsmf  47341  issmfle  47344  issmfgt  47355  smfadd  47364  decsmf  47366  issmfge  47369  smflimlem4  47373  smflim  47376  smfmul  47394  smflimsuplem2  47420  smflimsuplem5  47423  smflimsuplem7  47425  requad2  48270  uspgrlimlem1  48635  grlimedgclnbgr  48642  grlimgrtri  48650  gpgusgralem  48703  intubeu  49640  unilbeu  49641