Theorem cbvrabv 3428

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 2195 and ax-13 2406. (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 2848	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 644	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2835	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3419	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3419	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2798	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

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

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419

This theorem is used by:  rru  3744  knatar  7363  oeeulem  8589  cofon1  8660  ordtypecbv  9482  ordtypelem9  9491  inf3lema  9596  oemapso  9654  oemapvali  9656  tz9.12lem3  9764  cofsmo  10264  enfin2i  10316  fin23lem33  10340  isf32lem11  10358  zorn2g  10498  pwfseqlem1  10654  pwfseqlem3  10656  zsupss  12972  zmin  12979  rpnnen1  13018  hashbc  14503  wrd2f1tovbij  15016  01sqrexlem7  15318  divalglem5  16472  bitsfzolem  16509  smupp1  16555  gcdcllem3  16576  bezout  16618  eulerth  16859  odzval  16868  pcprecl  16916  pcprendvds  16917  pcpremul  16920  pceulem  16922  prmreclem1  16993  prmreclem5  16997  prmreclem6  16998  4sqlem19  17040  vdwnn  17075  hashbcval  17079  gsumvalx  18755  symgfixelq  19526  efgsdm  19823  efgsfo  19832  ablfaclem3  20182  ltbwe  22224  coe1mul2lem2  22458  smadiadetlem3  22854  pptbas  23194  conncompss  23619  ptcmplem5  24242  ustuqtop  24432  utopsnneip  24434  icccmplem2  25010  minveclem5  25621  ivth  25642  ovolicc2lem5  25709  ovolicc  25711  opnmbllem  25789  vitali  25801  itg2monolem3  25940  elqaa  26512  radcnvle  26612  pserdvlem2  26620  lgamgulmlem5  27226  lgamcvglem  27233  wilth  27264  ftalem6  27271  precsexlemcbv  28428  bdayons  28498  ttgval  29253  axcontlem11  29353  lfgredgge2  29503  usgredgleordALT  29613  nbusgrf1o  29750  cusgrexg  29823  cusgrfilem2  29835  cusgrfi  29837  vtxdushgrfvedglem  29868  vtxdushgrfvedg  29869  vtxdginducedm1  29922  finsumvtxdg2sstep  29928  wwlksnextbij  30280  rusgrnumwwlks  30355  clwlkclwwlkfolem  30387  clwlkclwwlken  30392  clwwlknscsh  30442  hashecclwwlkn1  30457  umgrhashecclwwlk  30458  clwlknf1oclwwlknlem2  30462  clwlknf1oclwwlkn  30464  frgrwopreglem5lem  30700  frgrregorufr0  30704  fusgreghash2wsp  30718  dlwwlknondlwlknonf1o  30745  ubthlem3  31253  htth  31299  fcobijfs  33095  fcobijfs2  33096  elrgspnsubrunlem1  33590  elrgspnsubrun  33592  1arithufd  33861  extvfvcl  33949  mplvrpmfgalem  33957  constrsuc  34151  constrcbvlem  34168  locfinreflem  34253  zarmxt1  34293  zarcmp  34295  ordtconnlem1  34337  dynkin  34581  ddemeas  34650  oddpwdc  34768  eulerpartgbij  34786  eulerpartlemn  34795  eulerpart  34796  ballotlemelo  34902  ballotleme  34911  ballotlem7  34950  reprsuc  35026  hgt750lema  35068  hgt750leme  35069  fineqvnttrclse  35553  onvf1odlem3  35605  subfacp1lem6  35690  erdsze  35707  cvmscbv  35763  cvmsiota  35782  cvmlift2lem13  35820  satfv1  35868  neibastop2  36905  weiunfrlem  37008  topdifinffin  38027  poimirlem27  38331  mblfinlem1  38341  mblfinlem2  38342  lclkrs2  42347  aks4d1  42889  sticksstones2  42947  eldioph4i  43572  rfovcnvf1od  44763  fsovrfovd  44768  fsovcnvlem  44772  nzss  45060  supminfxr2  46216  limcperiod  46377  cncfshiftioo  46639  ioodvbdlimc1lem2  46679  ioodvbdlimc2lem  46681  dvnprodlem1  46693  dvnprod  46696  itgiccshift  46727  itgperiod  46728  stoweidlem49  46796  fourierdlem41  46895  fourierdlem48  46901  fourierdlem49  46902  fourierdlem54  46907  fourierdlem65  46918  fourierdlem70  46923  fourierdlem71  46924  fourierdlem81  46934  fourierdlem89  46942  fourierdlem90  46943  fourierdlem91  46944  fourierdlem92  46945  fourierdlem96  46949  fourierdlem97  46950  fourierdlem98  46951  fourierdlem99  46952  fourierdlem100  46953  fourierdlem103  46956  fourierdlem104  46957  fourierdlem105  46958  fourierdlem108  46961  fourierdlem109  46962  fourierdlem110  46963  fourierdlem112  46965  fourierdlem113  46966  elaa2  46981  etransclem11  46992  etransc  47030  salexct  47081  subsaliuncl  47105  sge0fodjrnlem  47163  meadjiun  47213  ovnsubadd  47319  hoidmv1le  47341  hoidmvlelem3  47344  hoidmvlelem5  47346  ovnhoi  47350  hspmbllem3  47375  hspmbl  47376  opnvonmbl  47381  ovolval4lem2  47397  ovolval5lem2  47400  ovolval5lem3  47401  ovolval5  47402  ovnovol  47406  issmf  47475  incsmf  47489  issmfle  47492  issmfgt  47503  smfadd  47512  decsmf  47514  issmfge  47517  smflimlem4  47521  smflim  47524  smfmul  47542  smflimsuplem2  47568  smflimsuplem5  47571  smflimsuplem7  47573  requad2  48421  uspgrlimlem1  48786  grlimedgclnbgr  48793  grlimgrtri  48801  gpgusgralem  48854  intubeu  49795  unilbeu  49796