Theorem eleqtrri 2827

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 2738	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtri 2826	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 2701

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

This theorem is referenced by:  3eltr4i  2841  vex  3440  opi1  5411  opi2  5412  frrlem14  8232  seqomlem3  8374  nlim2  8408  oneo  8499  nnneo  8573  0elixp  8856  ac6sfi  9173  tz9.13  9687  rankval  9712  rankid  9729  ssrankr1  9731  rankel  9735  rankval3  9736  rankpw  9739  rankss  9745  ranksn  9750  rankuni2  9751  rankun  9752  rankpr  9753  rankop  9754  rankeq0  9757  rankr1b  9760  djuun  9822  dju1dif  10067  isfin4p1  10209  fin1a2lem4  10297  fin1a2lem6  10299  hsmexlem6  10325  dcomex  10341  axdc3lem4  10347  canthp1lem2  10547  pwxpndom2  10559  rankcf  10671  grutsk  10716  axgroth3  10725  inaprc  10730  1lt2pi  10799  pnfxr  11169  mnfxr  11172  1nn  12139  uzrdg0i  13866  axdc4uzlem  13890  ccat2s1p2  14537  wrdl3s3  14869  infcvgaux1i  15764  0bits  16350  sadcf  16364  prmreclem6  16833  fnpr2ob  17462  setcepi  17995  setc2obas  18001  setc2ohom  18002  cat1  18004  smndex1mnd  18784  smndex1id  18785  pwmnd  18811  grpss  18833  psgnunilem2  19374  psgnprfval2  19402  efgi0  19599  efgi1  19600  vrgpf  19647  vrgpinv  19648  frgpuptinv  19650  frgpup2  19655  frgpnabllem1  19752  dmdprdpr  19930  dprdpr  19931  pzriprnglem7  21394  pzriprnglem13  21400  pzriprng1ALT  21403  m2detleiblem3  22514  m2detleiblem4  22515  m2detleib  22516  leordtval2  23097  xpstopnlem1  23694  xpstopnlem2  23696  ptcmp  23943  tsmsfbas  24013  zcld  24700  sszcld  24704  abscncfALT  24816  iimulcn  24832  iimulcnOLD  24833  icopnfhmeo  24839  iccpnfhmeo  24841  xrhmeo  24842  cnstrcvs  25039  cncvs  25043  dveflem  25881  ftc1  25947  efopnlem2  26564  cxpcn3  26656  efrlim  26877  efrlimOLD  26878  precsexlem11  28124  1nns  28246  structvtxval  28966  usgrexmplef  29204  wwlks2onv  29898  elwwlks2ons3im  29899  umgrwwlks2on  29902  konigsberglem4  30199  hhshsslem2  31212  nonbooli  31595  nmopadjlei  32032  cshw1s2  32902  fzto1st  33045  cyc2fv1  33063  cyc3fv1  33079  cyc3fv2  33080  cyc3evpm  33092  1arithidom  33474  zringpid  33489  xrge0iifhmeo  33903  dya2iocbrsiga  34243  dya2icobrsiga  34244  fib0  34367  fib1  34368  coinflippvt  34453  prodfzo03  34571  circlevma  34610  circlemethhgt  34611  hgt750lemg  34622  hgt750lemb  34624  hgt750lema  34625  hgt750leme  34626  tgoldbachgtde  34628  tgoldbachgt  34631  bnj97  34833  bnj553  34865  bnj966  34911  bnj1442  35016  fineqvnttrclse  35077  subfacp1lem2a  35157  subfacp1lem5  35161  erdszelem5  35172  erdszelem8  35175  ex-sategoelel12  35404  rankeq1o  36149  0hf  36155  onint1  36427  bj-0eltag  36956  bj-minftyccb  37203  finxpreclem4  37372  fdc  37729  reheibor  37823  0prjspnlem  42600  0prjspnrel  42604  pw2f1ocnv  43014  onexoegt  43221  2omomeqom  43280  omnord1ex  43281  oege2  43284  oenord1ex  43292  oenord1  43293  oaomoencom  43294  oenassex  43295  comptiunov2i  43683  clsk1indlem4  44021  clsk1indlem1  44022  mnuprdlem3  44251  sucidALTVD  44847  sucidALT  44848  sucidVD  44849  wfaxnul  44974  wfaxinf2  44979  nregmodellem  44994  rfcnpre1  45001  eliuniincex  45091  iocopn  45505  icoopn  45510  islptre  45604  cnrefiisplem  45814  icccncfext  45872  fourierdlem103  46194  fourierdlem104  46195  iooborel  46336  upwordnul  46865  upwordsing  46869  sprsymrelfo  47485  sbgoldbo  47775  stgr1  47949  isubgr3stgrlem7  47960  gpg3kgrtriexlem5  48075  pglem  48079  grlimedgnedg  48119  0even  48225  2even  48227  2zrngamgm  48233  zlmodzxzldeplem3  48491  rrx2pxel  48700  rrx2pyel  48701  rrx2linesl  48732  2sphere0  48739  i0oii  48908  io1ii  48909  setc1onsubc  49591