Theorem cbvrabv 3493

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 2161 and ax-13 2390. (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 2897	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2891	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3149	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3149	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2856	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   = wceq 1537   ∈ wcel 2114  {cab 2801  {crab 3144

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1781  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-rab 3149

This theorem is referenced by:  rabrabi  3495  rru  3772  knatar  7112  oeeulem  8229  ordtypecbv  8983  ordtypelem9  8992  inf3lema  9089  oemapso  9147  oemapvali  9149  tz9.12lem3  9220  cofsmo  9693  enfin2i  9745  fin23lem33  9769  isf32lem11  9787  zorn2g  9927  pwfseqlem1  10082  pwfseqlem3  10084  zsupss  12340  zmin  12347  rpnnen1  12385  hashbc  13814  wrd2f1tovbij  14326  sqrlem7  14610  divalglem5  15750  bitsfzolem  15785  smupp1  15831  gcdcllem3  15852  bezout  15893  eulerth  16122  odzval  16130  pcprecl  16178  pcprendvds  16179  pcpremul  16182  pceulem  16184  prmreclem1  16254  prmreclem5  16258  prmreclem6  16259  4sqlem19  16301  vdwnn  16336  hashbcval  16340  gsumvalx  17888  symgfixelq  18563  efgsdm  18858  efgsfo  18867  ablfaclem3  19211  ltbwe  20255  coe1mul2lem2  20438  smadiadetlem3  21279  pptbas  21618  conncompss  22043  ptcmplem5  22666  ustuqtop  22857  utopsnneip  22859  icccmplem2  23433  minveclem5  24038  ivth  24057  ovolicc2lem5  24124  ovolicc  24126  opnmbllem  24204  vitali  24216  itg2monolem3  24355  elqaa  24913  radcnvle  25010  pserdvlem2  25018  lgamgulmlem5  25612  lgamcvglem  25619  wilth  25650  ftalem6  25657  ttgval  26663  axcontlem11  26762  lfgredgge2  26911  usgredgleordALT  27018  nbusgrf1o  27155  cusgrexg  27228  cusgrfilem2  27240  cusgrfi  27242  vtxdushgrfvedglem  27273  vtxdushgrfvedg  27274  vtxdginducedm1  27327  finsumvtxdg2sstep  27333  wwlksnextbij  27682  rusgrnumwwlks  27755  clwlkclwwlkfolem  27787  clwlkclwwlken  27792  clwwlknscsh  27843  hashecclwwlkn1  27858  umgrhashecclwwlk  27859  clwlknf1oclwwlknlem2  27863  clwlknf1oclwwlkn  27865  frgrwopreglem5lem  28101  frgrregorufr0  28105  fusgreghash2wsp  28119  dlwwlknondlwlknonf1o  28146  ubthlem3  28651  htth  28697  fcobijfs  30461  locfinreflem  31106  ordtconnlem1  31169  dynkin  31428  ddemeas  31497  oddpwdc  31614  eulerpartgbij  31632  eulerpartlemn  31641  eulerpart  31642  ballotlemelo  31747  ballotleme  31756  ballotlem7  31795  reprsuc  31888  hgt750lema  31930  hgt750leme  31931  subfacp1lem6  32434  erdsze  32451  cvmscbv  32507  cvmsiota  32526  cvmlift2lem13  32564  satfv1  32612  neibastop2  33711  topdifinffin  34631  poimirlem27  34921  mblfinlem1  34931  mblfinlem2  34932  lclkrs2  38678  eldioph4i  39416  rfovcnvf1od  40357  fsovrfovd  40362  fsovcnvlem  40366  nzss  40656  supminfxr2  41752  limcperiod  41916  cncfshiftioo  42182  ioodvbdlimc1lem2  42224  ioodvbdlimc2lem  42226  dvnprodlem1  42238  dvnprod  42241  itgiccshift  42272  itgperiod  42273  stoweidlem49  42341  fourierdlem41  42440  fourierdlem48  42446  fourierdlem49  42447  fourierdlem54  42452  fourierdlem65  42463  fourierdlem70  42468  fourierdlem71  42469  fourierdlem81  42479  fourierdlem89  42487  fourierdlem90  42488  fourierdlem91  42489  fourierdlem92  42490  fourierdlem96  42494  fourierdlem97  42495  fourierdlem98  42496  fourierdlem99  42497  fourierdlem100  42498  fourierdlem103  42501  fourierdlem104  42502  fourierdlem105  42503  fourierdlem108  42506  fourierdlem109  42507  fourierdlem110  42508  fourierdlem112  42510  fourierdlem113  42511  elaa2  42526  etransclem11  42537  etransc  42575  salexct  42624  subsaliuncl  42648  sge0fodjrnlem  42705  meadjiun  42755  ovnsubadd  42861  hoidmv1le  42883  hoidmvlelem3  42886  hoidmvlelem5  42888  ovnhoi  42892  hspmbllem3  42917  hspmbl  42918  opnvonmbl  42923  ovolval4lem2  42939  ovolval5lem2  42942  ovolval5lem3  42943  ovolval5  42944  ovnovol  42948  issmf  43012  incsmf  43026  issmfle  43029  issmfgt  43040  smfadd  43048  decsmf  43050  issmfge  43053  smflimlem4  43057  smflim  43060  smfmul  43077  smflimsuplem2  43102  smflimsuplem5  43105  smflimsuplem7  43107  requad2  43795