Theorem cbvrabv 3443

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 2155 and ax-13 2372. (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 2817	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2806	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3434	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3434	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2771	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  {cab 2710  {crab 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434

This theorem is referenced by:  rabrabiOLD  3457  rru  3776  knatar  7354  oeeulem  8601  cofon1  8671  ordtypecbv  9512  ordtypelem9  9521  inf3lema  9619  oemapso  9677  oemapvali  9679  tz9.12lem3  9784  cofsmo  10264  enfin2i  10316  fin23lem33  10340  isf32lem11  10358  zorn2g  10498  pwfseqlem1  10653  pwfseqlem3  10655  zsupss  12921  zmin  12928  rpnnen1  12967  hashbc  14412  wrd2f1tovbij  14911  01sqrexlem7  15195  divalglem5  16340  bitsfzolem  16375  smupp1  16421  gcdcllem3  16442  bezout  16485  eulerth  16716  odzval  16724  pcprecl  16772  pcprendvds  16773  pcpremul  16776  pceulem  16778  prmreclem1  16849  prmreclem5  16853  prmreclem6  16854  4sqlem19  16896  vdwnn  16931  hashbcval  16935  gsumvalx  18595  symgfixelq  19301  efgsdm  19598  efgsfo  19607  ablfaclem3  19957  ltbwe  21599  coe1mul2lem2  21790  smadiadetlem3  22170  pptbas  22511  conncompss  22937  ptcmplem5  23560  ustuqtop  23751  utopsnneip  23753  icccmplem2  24339  minveclem5  24950  ivth  24971  ovolicc2lem5  25038  ovolicc  25040  opnmbllem  25118  vitali  25130  itg2monolem3  25270  elqaa  25835  radcnvle  25932  pserdvlem2  25940  lgamgulmlem5  26537  lgamcvglem  26544  wilth  26575  ftalem6  26582  precsexlemcbv  27652  ttgval  28126  ttgvalOLD  28127  axcontlem11  28232  lfgredgge2  28384  usgredgleordALT  28491  nbusgrf1o  28628  cusgrexg  28701  cusgrfilem2  28713  cusgrfi  28715  vtxdushgrfvedglem  28746  vtxdushgrfvedg  28747  vtxdginducedm1  28800  finsumvtxdg2sstep  28806  wwlksnextbij  29156  rusgrnumwwlks  29228  clwlkclwwlkfolem  29260  clwlkclwwlken  29265  clwwlknscsh  29315  hashecclwwlkn1  29330  umgrhashecclwwlk  29331  clwlknf1oclwwlknlem2  29335  clwlknf1oclwwlkn  29337  frgrwopreglem5lem  29573  frgrregorufr0  29577  fusgreghash2wsp  29591  dlwwlknondlwlknonf1o  29618  ubthlem3  30125  htth  30171  fcobijfs  31948  locfinreflem  32820  zarmxt1  32860  zarcmp  32862  ordtconnlem1  32904  dynkin  33165  ddemeas  33234  oddpwdc  33353  eulerpartgbij  33371  eulerpartlemn  33380  eulerpart  33381  ballotlemelo  33486  ballotleme  33495  ballotlem7  33534  reprsuc  33627  hgt750lema  33669  hgt750leme  33670  subfacp1lem6  34176  erdsze  34193  cvmscbv  34249  cvmsiota  34268  cvmlift2lem13  34306  satfv1  34354  neibastop2  35246  topdifinffin  36229  poimirlem27  36515  mblfinlem1  36525  mblfinlem2  36526  lclkrs2  40411  aks4d1  40954  sticksstones2  40963  eldioph4i  41550  rfovcnvf1od  42755  fsovrfovd  42760  fsovcnvlem  42764  nzss  43076  supminfxr2  44179  limcperiod  44344  cncfshiftioo  44608  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  dvnprodlem1  44662  dvnprod  44665  itgiccshift  44696  itgperiod  44697  stoweidlem49  44765  fourierdlem41  44864  fourierdlem48  44870  fourierdlem49  44871  fourierdlem54  44876  fourierdlem65  44887  fourierdlem70  44892  fourierdlem71  44893  fourierdlem81  44903  fourierdlem89  44911  fourierdlem90  44912  fourierdlem91  44913  fourierdlem92  44914  fourierdlem96  44918  fourierdlem97  44919  fourierdlem98  44920  fourierdlem99  44921  fourierdlem100  44922  fourierdlem103  44925  fourierdlem104  44926  fourierdlem105  44927  fourierdlem108  44930  fourierdlem109  44931  fourierdlem110  44932  fourierdlem112  44934  fourierdlem113  44935  elaa2  44950  etransclem11  44961  etransc  44999  salexct  45050  subsaliuncl  45074  sge0fodjrnlem  45132  meadjiun  45182  ovnsubadd  45288  hoidmv1le  45310  hoidmvlelem3  45313  hoidmvlelem5  45315  ovnhoi  45319  hspmbllem3  45344  hspmbl  45345  opnvonmbl  45350  ovolval4lem2  45366  ovolval5lem2  45369  ovolval5lem3  45370  ovolval5  45371  ovnovol  45375  issmf  45444  incsmf  45458  issmfle  45461  issmfgt  45472  smfadd  45481  decsmf  45483  issmfge  45486  smflimlem4  45490  smflim  45493  smfmul  45511  smflimsuplem2  45537  smflimsuplem5  45540  smflimsuplem7  45542  requad2  46291  intubeu  47609  unilbeu  47610