Theorem eleqtrri 2828

Description: Substitution of equal classes into membership relation. (Contributed by NM, 15-Jul-1993.)

Hypotheses

Ref	Expression
eleqtrri.1	⊢ 𝐴 ∈ 𝐵
eleqtrri.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
eleqtrri	⊢ 𝐴 ∈ 𝐶

Proof of Theorem eleqtrri

Step	Hyp	Ref	Expression
1		eleqtrri.1	. 2 ⊢ 𝐴 ∈ 𝐵
2		eleqtrri.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2739	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtri 2827	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1540   ∈ wcel 2109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-clel 2804

This theorem is referenced by:  3eltr4i  2842  vex  3454  opi1  5431  opi2  5432  frrlem14  8281  seqomlem3  8423  nlim2  8457  oneo  8548  nnneo  8622  0elixp  8905  ac6sfi  9238  tz9.13  9751  rankval  9776  rankid  9793  ssrankr1  9795  rankel  9799  rankval3  9800  rankpw  9803  rankss  9809  ranksn  9814  rankuni2  9815  rankun  9816  rankpr  9817  rankop  9818  rankeq0  9821  rankr1b  9824  djuun  9886  dju1dif  10133  isfin4p1  10275  fin1a2lem4  10363  fin1a2lem6  10365  hsmexlem6  10391  dcomex  10407  axdc3lem4  10413  canthp1lem2  10613  pwxpndom2  10625  rankcf  10737  grutsk  10782  axgroth3  10791  inaprc  10796  1lt2pi  10865  pnfxr  11235  mnfxr  11238  1nn  12204  uzrdg0i  13931  axdc4uzlem  13955  ccat2s1p2  14602  wrdl3s3  14935  infcvgaux1i  15830  0bits  16416  sadcf  16430  prmreclem6  16899  fnpr2ob  17528  setcepi  18057  setc2obas  18063  setc2ohom  18064  cat1  18066  smndex1mnd  18844  smndex1id  18845  pwmnd  18871  grpss  18893  psgnunilem2  19432  psgnprfval2  19460  efgi0  19657  efgi1  19658  vrgpf  19705  vrgpinv  19706  frgpuptinv  19708  frgpup2  19713  frgpnabllem1  19810  dmdprdpr  19988  dprdpr  19989  pzriprnglem7  21404  pzriprnglem13  21410  pzriprng1ALT  21413  m2detleiblem3  22523  m2detleiblem4  22524  m2detleib  22525  leordtval2  23106  xpstopnlem1  23703  xpstopnlem2  23705  ptcmp  23952  tsmsfbas  24022  zcld  24709  sszcld  24713  abscncfALT  24825  iimulcn  24841  iimulcnOLD  24842  icopnfhmeo  24848  iccpnfhmeo  24850  xrhmeo  24851  cnstrcvs  25048  cncvs  25052  dveflem  25890  ftc1  25956  efopnlem2  26573  cxpcn3  26665  efrlim  26886  efrlimOLD  26887  precsexlem11  28126  1nns  28248  structvtxval  28955  usgrexmplef  29193  wwlks2onv  29890  elwwlks2ons3im  29891  umgrwwlks2on  29894  konigsberglem4  30191  hhshsslem2  31204  nonbooli  31587  nmopadjlei  32024  cshw1s2  32889  fzto1st  33067  cyc2fv1  33085  cyc3fv1  33101  cyc3fv2  33102  cyc3evpm  33114  1arithidom  33515  zringpid  33530  xrge0iifhmeo  33933  dya2iocbrsiga  34273  dya2icobrsiga  34274  fib0  34397  fib1  34398  coinflippvt  34483  prodfzo03  34601  circlevma  34640  circlemethhgt  34641  hgt750lemg  34652  hgt750lemb  34654  hgt750lema  34655  hgt750leme  34656  tgoldbachgtde  34658  tgoldbachgt  34661  bnj97  34863  bnj553  34895  bnj966  34941  bnj1442  35046  subfacp1lem2a  35174  subfacp1lem5  35178  erdszelem5  35189  erdszelem8  35192  ex-sategoelel12  35421  rankeq1o  36166  0hf  36172  onint1  36444  bj-0eltag  36973  bj-minftyccb  37220  finxpreclem4  37389  fdc  37746  reheibor  37840  0prjspnlem  42618  0prjspnrel  42622  pw2f1ocnv  43033  onexoegt  43240  2omomeqom  43299  omnord1ex  43300  oege2  43303  oenord1ex  43311  oenord1  43312  oaomoencom  43313  oenassex  43314  comptiunov2i  43702  clsk1indlem4  44040  clsk1indlem1  44041  mnuprdlem3  44270  sucidALTVD  44866  sucidALT  44867  sucidVD  44868  wfaxnul  44993  wfaxinf2  44998  nregmodellem  45013  rfcnpre1  45020  eliuniincex  45110  iocopn  45525  icoopn  45530  islptre  45624  cnrefiisplem  45834  icccncfext  45892  fourierdlem103  46214  fourierdlem104  46215  iooborel  46356  upwordnul  46885  upwordsing  46889  sprsymrelfo  47502  sbgoldbo  47792  stgr1  47964  isubgr3stgrlem7  47975  gpg3kgrtriexlem5  48082  pglem  48086  0even  48229  2even  48231  2zrngamgm  48237  zlmodzxzldeplem3  48495  rrx2pxel  48704  rrx2pyel  48705  rrx2linesl  48736  2sphere0  48743  i0oii  48912  io1ii  48913  setc1onsubc  49595