Theorem cbvrabv 3413

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 2153 and ax-13 2370. (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 2819	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 631	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2809	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3404	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3404	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2774	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1540   ∈ wcel 2105  {cab 2713  {crab 3403

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-rab 3404

This theorem is referenced by:  rabrabiOLD  3427  rru  3724  knatar  7278  oeeulem  8495  ordtypecbv  9366  ordtypelem9  9375  inf3lema  9473  oemapso  9531  oemapvali  9533  tz9.12lem3  9638  cofsmo  10118  enfin2i  10170  fin23lem33  10194  isf32lem11  10212  zorn2g  10352  pwfseqlem1  10507  pwfseqlem3  10509  zsupss  12770  zmin  12777  rpnnen1  12816  hashbc  14257  wrd2f1tovbij  14766  sqrlem7  15051  divalglem5  16197  bitsfzolem  16232  smupp1  16278  gcdcllem3  16299  bezout  16342  eulerth  16573  odzval  16581  pcprecl  16629  pcprendvds  16630  pcpremul  16633  pceulem  16635  prmreclem1  16706  prmreclem5  16710  prmreclem6  16711  4sqlem19  16753  vdwnn  16788  hashbcval  16792  gsumvalx  18449  symgfixelq  19129  efgsdm  19423  efgsfo  19432  ablfaclem3  19777  ltbwe  21343  coe1mul2lem2  21537  smadiadetlem3  21915  pptbas  22256  conncompss  22682  ptcmplem5  23305  ustuqtop  23496  utopsnneip  23498  icccmplem2  24084  minveclem5  24695  ivth  24716  ovolicc2lem5  24783  ovolicc  24785  opnmbllem  24863  vitali  24875  itg2monolem3  25015  elqaa  25580  radcnvle  25677  pserdvlem2  25685  lgamgulmlem5  26280  lgamcvglem  26287  wilth  26318  ftalem6  26325  ttgval  27466  ttgvalOLD  27467  axcontlem11  27572  lfgredgge2  27724  usgredgleordALT  27831  nbusgrf1o  27968  cusgrexg  28041  cusgrfilem2  28053  cusgrfi  28055  vtxdushgrfvedglem  28086  vtxdushgrfvedg  28087  vtxdginducedm1  28140  finsumvtxdg2sstep  28146  wwlksnextbij  28496  rusgrnumwwlks  28568  clwlkclwwlkfolem  28600  clwlkclwwlken  28605  clwwlknscsh  28655  hashecclwwlkn1  28670  umgrhashecclwwlk  28671  clwlknf1oclwwlknlem2  28675  clwlknf1oclwwlkn  28677  frgrwopreglem5lem  28913  frgrregorufr0  28917  fusgreghash2wsp  28931  dlwwlknondlwlknonf1o  28958  ubthlem3  29463  htth  29509  fcobijfs  31286  locfinreflem  32029  zarmxt1  32069  zarcmp  32071  ordtconnlem1  32113  dynkin  32374  ddemeas  32443  oddpwdc  32562  eulerpartgbij  32580  eulerpartlemn  32589  eulerpart  32590  ballotlemelo  32695  ballotleme  32704  ballotlem7  32743  reprsuc  32836  hgt750lema  32878  hgt750leme  32879  subfacp1lem6  33387  erdsze  33404  cvmscbv  33460  cvmsiota  33479  cvmlift2lem13  33517  satfv1  33565  neibastop2  34641  topdifinffin  35617  poimirlem27  35902  mblfinlem1  35912  mblfinlem2  35913  lclkrs2  39801  aks4d1  40344  sticksstones2  40353  eldioph4i  40884  rfovcnvf1od  41922  fsovrfovd  41927  fsovcnvlem  41931  nzss  42245  supminfxr2  43333  limcperiod  43494  cncfshiftioo  43758  ioodvbdlimc1lem2  43798  ioodvbdlimc2lem  43800  dvnprodlem1  43812  dvnprod  43815  itgiccshift  43846  itgperiod  43847  stoweidlem49  43915  fourierdlem41  44014  fourierdlem48  44020  fourierdlem49  44021  fourierdlem54  44026  fourierdlem65  44037  fourierdlem70  44042  fourierdlem71  44043  fourierdlem81  44053  fourierdlem89  44061  fourierdlem90  44062  fourierdlem91  44063  fourierdlem92  44064  fourierdlem96  44068  fourierdlem97  44069  fourierdlem98  44070  fourierdlem99  44071  fourierdlem100  44072  fourierdlem103  44075  fourierdlem104  44076  fourierdlem105  44077  fourierdlem108  44080  fourierdlem109  44081  fourierdlem110  44082  fourierdlem112  44084  fourierdlem113  44085  elaa2  44100  etransclem11  44111  etransc  44149  salexct  44198  subsaliuncl  44222  sge0fodjrnlem  44280  meadjiun  44330  ovnsubadd  44436  hoidmv1le  44458  hoidmvlelem3  44461  hoidmvlelem5  44463  ovnhoi  44467  hspmbllem3  44492  hspmbl  44493  opnvonmbl  44498  ovolval4lem2  44514  ovolval5lem2  44517  ovolval5lem3  44518  ovolval5  44519  ovnovol  44523  issmf  44592  incsmf  44606  issmfle  44609  issmfgt  44620  smfadd  44629  decsmf  44631  issmfge  44634  smflimlem4  44638  smflim  44641  smfmul  44659  smflimsuplem2  44685  smflimsuplem5  44688  smflimsuplem7  44690  requad2  45415  intubeu  46610  unilbeu  46611