Theorem cbvrabv 3405

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 2160 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 2814	. . . 4 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ 𝐴 ↔ 𝑦 ∈ 𝐴))
2		cbvrabv.1	. . . 4 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜓))
3	1, 2	anbi12d 632	. . 3 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ 𝐴 ∧ 𝜑) ↔ (𝑦 ∈ 𝐴 ∧ 𝜓)))
4	3	cbvabv 2801	. 2 ⊢ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
5		df-rab 3396	. 2 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝜑)}
6		df-rab 3396	. 2 ⊢ {𝑦 ∈ 𝐴 ∣ 𝜓} = {𝑦 ∣ (𝑦 ∈ 𝐴 ∧ 𝜓)}
7	4, 5, 6	3eqtr4i 2764	1 ⊢ {𝑥 ∈ 𝐴 ∣ 𝜑} = {𝑦 ∈ 𝐴 ∣ 𝜓}

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2111  {cab 2709  {crab 3395

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396

This theorem is referenced by:  rru  3733  knatar  7286  oeeulem  8511  cofon1  8582  ordtypecbv  9398  ordtypelem9  9407  inf3lema  9509  oemapso  9567  oemapvali  9569  tz9.12lem3  9677  cofsmo  10155  enfin2i  10207  fin23lem33  10231  isf32lem11  10249  zorn2g  10389  pwfseqlem1  10544  pwfseqlem3  10546  zsupss  12830  zmin  12837  rpnnen1  12876  hashbc  14355  wrd2f1tovbij  14862  01sqrexlem7  15150  divalglem5  16303  bitsfzolem  16340  smupp1  16386  gcdcllem3  16407  bezout  16449  eulerth  16689  odzval  16698  pcprecl  16746  pcprendvds  16747  pcpremul  16750  pceulem  16752  prmreclem1  16823  prmreclem5  16827  prmreclem6  16828  4sqlem19  16870  vdwnn  16905  hashbcval  16909  gsumvalx  18579  symgfixelq  19340  efgsdm  19637  efgsfo  19646  ablfaclem3  19996  ltbwe  21974  coe1mul2lem2  22177  smadiadetlem3  22578  pptbas  22918  conncompss  23343  ptcmplem5  23966  ustuqtop  24156  utopsnneip  24158  icccmplem2  24734  minveclem5  25355  ivth  25377  ovolicc2lem5  25444  ovolicc  25446  opnmbllem  25524  vitali  25536  itg2monolem3  25675  elqaa  26252  radcnvle  26351  pserdvlem2  26360  lgamgulmlem5  26965  lgamcvglem  26972  wilth  27003  ftalem6  27010  precsexlemcbv  28139  bdayon  28204  ttgval  28848  axcontlem11  28947  lfgredgge2  29097  usgredgleordALT  29207  nbusgrf1o  29344  cusgrexg  29417  cusgrfilem2  29430  cusgrfi  29432  vtxdushgrfvedglem  29463  vtxdushgrfvedg  29464  vtxdginducedm1  29517  finsumvtxdg2sstep  29523  wwlksnextbij  29875  rusgrnumwwlks  29947  clwlkclwwlkfolem  29979  clwlkclwwlken  29984  clwwlknscsh  30034  hashecclwwlkn1  30049  umgrhashecclwwlk  30050  clwlknf1oclwwlknlem2  30054  clwlknf1oclwwlkn  30056  frgrwopreglem5lem  30292  frgrregorufr0  30296  fusgreghash2wsp  30310  dlwwlknondlwlknonf1o  30337  ubthlem3  30844  htth  30890  fcobijfs  32696  fcobijfs2  32697  elrgspnsubrunlem1  33206  elrgspnsubrun  33208  1arithufd  33505  mplvrpmfgalem  33566  constrsuc  33743  constrcbvlem  33760  locfinreflem  33845  zarmxt1  33885  zarcmp  33887  ordtconnlem1  33929  dynkin  34172  ddemeas  34241  oddpwdc  34359  eulerpartgbij  34377  eulerpartlemn  34386  eulerpart  34387  ballotlemelo  34493  ballotleme  34502  ballotlem7  34541  reprsuc  34620  hgt750lema  34662  hgt750leme  34663  fineqvnttrclse  35136  onvf1odlem3  35141  subfacp1lem6  35221  erdsze  35238  cvmscbv  35294  cvmsiota  35313  cvmlift2lem13  35351  satfv1  35399  neibastop2  36395  weiunfrlem  36498  topdifinffin  37382  poimirlem27  37687  mblfinlem1  37697  mblfinlem2  37698  lclkrs2  41579  aks4d1  42122  sticksstones2  42180  eldioph4i  42845  rfovcnvf1od  44037  fsovrfovd  44042  fsovcnvlem  44046  nzss  44350  supminfxr2  45507  limcperiod  45668  cncfshiftioo  45930  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  dvnprodlem1  45984  dvnprod  45987  itgiccshift  46018  itgperiod  46019  stoweidlem49  46087  fourierdlem41  46186  fourierdlem48  46192  fourierdlem49  46193  fourierdlem54  46198  fourierdlem65  46209  fourierdlem70  46214  fourierdlem71  46215  fourierdlem81  46225  fourierdlem89  46233  fourierdlem90  46234  fourierdlem91  46235  fourierdlem92  46236  fourierdlem96  46240  fourierdlem97  46241  fourierdlem98  46242  fourierdlem99  46243  fourierdlem100  46244  fourierdlem103  46247  fourierdlem104  46248  fourierdlem105  46249  fourierdlem108  46252  fourierdlem109  46253  fourierdlem110  46254  fourierdlem112  46256  fourierdlem113  46257  elaa2  46272  etransclem11  46283  etransc  46321  salexct  46372  subsaliuncl  46396  sge0fodjrnlem  46454  meadjiun  46504  ovnsubadd  46610  hoidmv1le  46632  hoidmvlelem3  46635  hoidmvlelem5  46637  ovnhoi  46641  hspmbllem3  46666  hspmbl  46667  opnvonmbl  46672  ovolval4lem2  46688  ovolval5lem2  46691  ovolval5lem3  46692  ovolval5  46693  ovnovol  46697  issmf  46766  incsmf  46780  issmfle  46783  issmfgt  46794  smfadd  46803  decsmf  46805  issmfge  46808  smflimlem4  46812  smflim  46815  smfmul  46833  smflimsuplem2  46859  smflimsuplem5  46862  smflimsuplem7  46864  requad2  47654  uspgrlimlem1  48019  grlimedgclnbgr  48026  grlimgrtri  48034  gpgusgralem  48087  intubeu  49015  unilbeu  49016