Theorem eleqtrri 2840

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 2749	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtri 2839	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1542   ∈ wcel 2110

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1787  df-cleq 2732  df-clel 2818

This theorem is referenced by:  3eltr4i  2854  vex  3435  vexOLD  3436  opi1  5387  opi2  5388  frrlem14  8106  wfrlem14OLD  8144  wfrlem16OLD  8146  seqomlem3  8274  oneo  8397  nnneo  8468  0elixp  8700  ac6sfi  9036  tz9.13  9550  rankval  9575  rankid  9592  ssrankr1  9594  rankel  9598  rankval3  9599  rankpw  9602  rankss  9608  ranksn  9613  rankuni2  9614  rankun  9615  rankpr  9616  rankop  9617  rankeq0  9620  rankr1b  9623  djuun  9685  dju1dif  9929  isfin4p1  10072  fin1a2lem4  10160  fin1a2lem6  10162  hsmexlem6  10188  dcomex  10204  axdc3lem4  10210  canthp1lem2  10410  pwxpndom2  10422  rankcf  10534  grutsk  10579  axgroth3  10588  inaprc  10593  1lt2pi  10662  pnfxr  11030  mnfxr  11033  1nn  11984  uzrdg0i  13677  axdc4uzlem  13701  ccat2s1p2  14335  ccat2s1p2OLD  14337  wrdl3s3  14675  infcvgaux1i  15567  0bits  16144  sadcf  16158  prmreclem6  16620  fnpr2ob  17267  setcepi  17801  setc2obas  17807  setc2ohom  17808  cat1  17810  smndex1mnd  18547  smndex1id  18548  pwmnd  18574  grpss  18595  psgnunilem2  19101  psgnprfval2  19129  efgi0  19324  efgi1  19325  vrgpf  19372  vrgpinv  19373  frgpuptinv  19375  frgpup2  19380  frgpnabllem1  19472  dmdprdpr  19650  dprdpr  19651  m2detleiblem3  21776  m2detleiblem4  21777  m2detleib  21778  leordtval2  22361  xpstopnlem1  22958  xpstopnlem2  22960  ptcmp  23207  tsmsfbas  23277  zcld  23974  sszcld  23978  abscncfALT  24085  iimulcn  24099  icopnfhmeo  24104  iccpnfhmeo  24106  xrhmeo  24107  cnstrcvs  24302  cncvs  24306  dveflem  25141  ftc1  25204  efopnlem2  25810  cxpcn3  25899  efrlim  26117  structvtxval  27389  usgrexmplef  27624  wwlks2onv  28314  elwwlks2ons3im  28315  umgrwwlks2on  28318  konigsberglem4  28615  hhshsslem2  29626  nonbooli  30009  nmopadjlei  30446  cshw1s2  31228  fzto1st  31366  cyc2fv1  31384  cyc3fv1  31400  cyc3fv2  31401  cyc3evpm  31413  xrge0iifhmeo  31882  dya2iocbrsiga  32238  dya2icobrsiga  32239  fib0  32362  fib1  32363  coinflippvt  32447  prodfzo03  32579  circlevma  32618  circlemethhgt  32619  hgt750lemg  32630  hgt750lemb  32632  hgt750lema  32633  hgt750leme  32634  tgoldbachgtde  32636  tgoldbachgt  32639  bnj97  32842  bnj553  32874  bnj966  32920  bnj1442  33025  subfacp1lem2a  33138  subfacp1lem5  33142  erdszelem5  33153  erdszelem8  33156  ex-sategoelel12  33385  rankeq1o  34469  0hf  34475  onint1  34634  bj-0eltag  35164  bj-minftyccb  35392  finxpreclem4  35561  fdc  35899  reheibor  35993  0prjspnlem  40457  0prjspnrel  40461  pw2f1ocnv  40856  comptiunov2i  41284  clsk1indlem4  41624  clsk1indlem1  41625  mnuprdlem3  41862  sucidALTVD  42460  sucidALT  42461  sucidVD  42462  rfcnpre1  42532  eliuniincex  42629  iocopn  43029  icoopn  43034  islptre  43131  cnrefiisplem  43341  icccncfext  43399  fourierdlem103  43721  fourierdlem104  43722  iooborel  43861  sprsymrelfo  44918  sbgoldbo  45208  0even  45458  2even  45460  2zrngamgm  45466  zlmodzxzldeplem3  45812  rrx2pxel  46026  rrx2pyel  46027  rrx2linesl  46058  2sphere0  46065  i0oii  46182  io1ii  46183  upwordnul  46481