Theorem cbvrabv 3423

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 2194 and ax-13 2402. (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 2844	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2831	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3414	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3414	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2794	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

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

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414

This theorem is used by:  rru  3737  knatar  7365  oeeulem  8603  cofon1  8674  ordtypecbv  9504  ordtypelem9  9513  inf3lema  9618  oemapso  9676  oemapvali  9678  tz9.12lem3  9789  cofsmo  10340  enfin2i  10392  fin23lem33  10416  isf32lem11  10434  zorn2g  10574  pwfseqlem1  10736  pwfseqlem3  10738  zsupss  13057  zmin  13064  rpnnen1  13104  hashbc  14591  wrd2f1tovbij  15106  01sqrexlem7  15408  divalglem5  16560  bitsfzolem  16597  smupp1  16643  gcdcllem3  16664  bezout  16709  eulerth  16953  odzval  16962  pcprecl  17010  pcprendvds  17011  pcpremul  17014  pceulem  17016  prmreclem1  17087  prmreclem5  17091  prmreclem6  17092  4sqlem19  17134  vdwnn  17169  hashbcval  17173  gsumvalx  18858  symgfixelq  19640  efgsdm  19937  efgsfo  19946  ablfaclem3  20296  ltbwe  22346  coe1mul2lem2  22580  smadiadetlem3  22976  pptbas  23319  conncompss  23744  ptcmplem5  24368  ustuqtop  24558  utopsnneip  24560  icccmplem2  25136  minveclem5  25747  ivth  25768  ovolicc2lem5  25835  ovolicc  25837  opnmbllem  25915  vitali  25927  itg2monolem3  26066  elqaa  26638  radcnvle  26740  pserdvlem2  26748  lgamgulmlem5  27353  lgamcvglem  27360  wilth  27391  ftalem6  27398  precsexlemcbv  28585  bdayons  28655  ttgval  29445  axcontlem11  29545  lfgredgge2  29695  usgredgleordALT  29808  nbusgrf1o  29945  cusgrexg  30018  cusgrfilem2  30030  cusgrfi  30032  vtxdushgrfvedglem  30063  vtxdushgrfvedg  30064  vtxdginducedm1  30117  finsumvtxdg2sstep  30123  wwlksnextbij  30484  rusgrnumwwlks  30559  clwlkclwwlkfolem  30591  clwlkclwwlken  30596  clwwlknscsh  30646  hashecclwwlkn1  30661  umgrhashecclwwlk  30662  clwlknf1oclwwlknlem2  30666  clwlknf1oclwwlkn  30668  frgrwopreglem5lem  30914  frgrregorufr0  30918  fusgreghash2wsp  30932  dlwwlknondlwlknonf1o  30959  ubthlem3  31467  htth  31513  fcobijfs  33306  fcobijfs2  33307  elrgspnsubrunlem1  33801  elrgspnsubrun  33803  1arithufd  34073  extvfvcl  34161  mplvrpmfgalem  34169  constrsuc  34363  constrcbvlem  34380  locfinreflem  34465  zarmxt1  34505  zarcmp  34507  ordtconnlem1  34549  dynkin  34793  ddemeas  34862  oddpwdc  34979  eulerpartgbij  34997  eulerpartlemn  35006  eulerpart  35007  ballotlemelo  35113  ballotleme  35122  ballotlem7  35161  reprsuc  35237  hgt750lema  35279  hgt750leme  35280  fineqvnttrclse  35775  onvf1odlem3  35867  subfacp1lem6  35929  erdsze  35946  cvmscbv  36002  cvmsiota  36021  cvmlift2lem13  36059  satfv1  36107  neibastop2  37129  weiunfrlem  37232  topdifinffin  38251  poimirlem27  38545  mblfinlem1  38555  mblfinlem2  38556  lclkrs2  42577  aks4d1  43119  sticksstones2  43177  eldioph4i  43798  rfovcnvf1od  44989  fsovrfovd  44994  fsovcnvlem  44998  nzss  45286  supminfxr2  46448  limcperiod  46609  cncfshiftioo  46871  ioodvbdlimc1lem2  46911  ioodvbdlimc2lem  46913  dvnprodlem1  46925  dvnprod  46928  itgiccshift  46959  itgperiod  46960  stoweidlem49  47028  fourierdlem41  47127  fourierdlem48  47133  fourierdlem49  47134  fourierdlem54  47139  fourierdlem65  47150  fourierdlem70  47155  fourierdlem71  47156  fourierdlem81  47166  fourierdlem89  47174  fourierdlem90  47175  fourierdlem91  47176  fourierdlem92  47177  fourierdlem96  47181  fourierdlem97  47182  fourierdlem98  47183  fourierdlem99  47184  fourierdlem100  47185  fourierdlem103  47188  fourierdlem104  47189  fourierdlem105  47190  fourierdlem108  47193  fourierdlem109  47194  fourierdlem110  47195  fourierdlem112  47197  fourierdlem113  47198  elaa2  47213  etransclem11  47224  etransc  47262  salexct  47313  subsaliuncl  47337  sge0fodjrnlem  47395  meadjiun  47445  ovnsubadd  47551  hoidmv1le  47573  hoidmvlelem3  47576  hoidmvlelem5  47578  ovnhoi  47582  hspmbllem3  47607  hspmbl  47608  opnvonmbl  47613  ovolval4lem2  47629  ovolval5lem2  47632  ovolval5lem3  47633  ovolval5  47634  ovnovol  47638  issmf  47707  incsmf  47721  issmfle  47724  issmfgt  47735  smfadd  47744  decsmf  47746  issmfge  47749  smflimlem4  47753  smflim  47756  smfmul  47774  smflimsuplem2  47800  smflimsuplem5  47803  smflimsuplem7  47805  requad2  48690  uspgrlimlem1  49055  grlimedgclnbgr  49062  grlimgrtri  49070  gpgusgralem  49123  intubeu  50061  unilbeu  50062