Theorem eleqtrri 2836

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

Syntax hints:   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-clel 2812

This theorem is referenced by:  3eltr4i  2850  vex  3434  opi1  5417  opi2  5418  frrlem14  8243  seqomlem3  8385  nlim2  8419  oneo  8510  nnneo  8585  0elixp  8871  ac6sfi  9188  tz9.13  9709  rankval  9734  rankid  9751  ssrankr1  9753  rankel  9757  rankval3  9758  rankpw  9761  rankss  9767  ranksn  9772  rankuni2  9773  rankun  9774  rankpr  9775  rankop  9776  rankeq0  9779  rankr1b  9782  djuun  9844  dju1dif  10089  isfin4p1  10231  fin1a2lem4  10319  fin1a2lem6  10321  hsmexlem6  10347  dcomex  10363  axdc3lem4  10369  canthp1lem2  10570  pwxpndom2  10582  rankcf  10694  grutsk  10739  axgroth3  10748  inaprc  10753  1lt2pi  10822  pnfxr  11193  mnfxr  11196  1nn  12179  uzrdg0i  13915  axdc4uzlem  13939  ccat2s1p2  14587  wrdl3s3  14918  infcvgaux1i  15816  0bits  16402  sadcf  16416  prmreclem6  16886  fnpr2ob  17516  setcepi  18049  setc2obas  18055  setc2ohom  18056  cat1  18058  smndex1mnd  18875  smndex1id  18876  pwmnd  18902  grpss  18924  psgnunilem2  19464  psgnprfval2  19492  efgi0  19689  efgi1  19690  vrgpf  19737  vrgpinv  19738  frgpuptinv  19740  frgpup2  19745  frgpnabllem1  19842  dmdprdpr  20020  dprdpr  20021  pzriprnglem7  21480  pzriprnglem13  21486  pzriprng1ALT  21489  m2detleiblem3  22607  m2detleiblem4  22608  m2detleib  22609  leordtval2  23190  xpstopnlem1  23787  xpstopnlem2  23789  ptcmp  24036  tsmsfbas  24106  zcld  24792  sszcld  24796  abscncfALT  24904  iimulcn  24918  icopnfhmeo  24923  iccpnfhmeo  24925  xrhmeo  24926  cnstrcvs  25121  cncvs  25125  dveflem  25959  ftc1  26022  efopnlem2  26637  cxpcn3  26728  efrlim  26949  efrlimOLD  26950  precsexlem11  28226  1nns  28358  structvtxval  29107  usgrexmplef  29345  wwlks2onv  30039  elwwlks2ons3im  30040  usgrwwlks2on  30044  umgrwwlks2on  30045  konigsberglem4  30343  hhshsslem2  31357  nonbooli  31740  nmopadjlei  32177  cshw1s2  33038  fzto1st  33182  cyc2fv1  33200  cyc3fv1  33216  cyc3fv2  33217  cyc3evpm  33229  1arithidom  33615  zringpid  33630  vieta  33742  xrge0iifhmeo  34099  dya2iocbrsiga  34438  dya2icobrsiga  34439  fib0  34562  fib1  34563  coinflippvt  34648  prodfzo03  34766  circlevma  34805  circlemethhgt  34806  hgt750lemg  34817  hgt750lemb  34819  hgt750lema  34820  hgt750leme  34821  tgoldbachgtde  34823  tgoldbachgt  34826  bnj97  35027  bnj553  35059  bnj966  35105  bnj1442  35210  fineqvnttrclse  35287  fineqvinfep  35288  subfacp1lem2a  35381  subfacp1lem5  35385  erdszelem5  35396  erdszelem8  35399  ex-sategoelel12  35628  rankeq1o  36372  0hf  36378  onint1  36650  regsfromunir1  36741  bj-0eltag  37304  bj-minftyccb  37558  finxpreclem4  37727  fdc  38083  reheibor  38177  0prjspnlem  43073  0prjspnrel  43077  pw2f1ocnv  43486  onexoegt  43693  2omomeqom  43752  omnord1ex  43753  oege2  43756  oenord1ex  43764  oenord1  43765  oaomoencom  43766  oenassex  43767  comptiunov2i  44154  clsk1indlem4  44492  clsk1indlem1  44493  mnuprdlem3  44722  sucidALTVD  45317  sucidALT  45318  sucidVD  45319  wfaxnul  45444  wfaxinf2  45449  nregmodellem  45464  rfcnpre1  45471  eliuniincex  45560  iocopn  45971  icoopn  45976  islptre  46070  cnrefiisplem  46278  icccncfext  46336  fourierdlem103  46658  fourierdlem104  46659  iooborel  46800  sprsymrelfo  47972  sbgoldbo  48278  stgr1  48452  isubgr3stgrlem7  48463  gpg3kgrtriexlem5  48578  pglem  48582  grlimedgnedg  48622  0even  48728  2even  48730  2zrngamgm  48736  zlmodzxzldeplem3  48993  rrx2pxel  49202  rrx2pyel  49203  rrx2linesl  49234  2sphere0  49241  i0oii  49410  io1ii  49411  setc1onsubc  50092