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  3448  opi1  5423  opi2  5424  frrlem14  8255  seqomlem3  8397  nlim2  8431  oneo  8522  nnneo  8596  0elixp  8879  ac6sfi  9207  tz9.13  9720  rankval  9745  rankid  9762  ssrankr1  9764  rankel  9768  rankval3  9769  rankpw  9772  rankss  9778  ranksn  9783  rankuni2  9784  rankun  9785  rankpr  9786  rankop  9787  rankeq0  9790  rankr1b  9793  djuun  9855  dju1dif  10102  isfin4p1  10244  fin1a2lem4  10332  fin1a2lem6  10334  hsmexlem6  10360  dcomex  10376  axdc3lem4  10382  canthp1lem2  10582  pwxpndom2  10594  rankcf  10706  grutsk  10751  axgroth3  10760  inaprc  10765  1lt2pi  10834  pnfxr  11204  mnfxr  11207  1nn  12173  uzrdg0i  13900  axdc4uzlem  13924  ccat2s1p2  14571  wrdl3s3  14904  infcvgaux1i  15799  0bits  16385  sadcf  16399  prmreclem6  16868  fnpr2ob  17497  setcepi  18030  setc2obas  18036  setc2ohom  18037  cat1  18039  smndex1mnd  18819  smndex1id  18820  pwmnd  18846  grpss  18868  psgnunilem2  19409  psgnprfval2  19437  efgi0  19634  efgi1  19635  vrgpf  19682  vrgpinv  19683  frgpuptinv  19685  frgpup2  19690  frgpnabllem1  19787  dmdprdpr  19965  dprdpr  19966  pzriprnglem7  21429  pzriprnglem13  21435  pzriprng1ALT  21438  m2detleiblem3  22549  m2detleiblem4  22550  m2detleib  22551  leordtval2  23132  xpstopnlem1  23729  xpstopnlem2  23731  ptcmp  23978  tsmsfbas  24048  zcld  24735  sszcld  24739  abscncfALT  24851  iimulcn  24867  iimulcnOLD  24868  icopnfhmeo  24874  iccpnfhmeo  24876  xrhmeo  24877  cnstrcvs  25074  cncvs  25078  dveflem  25916  ftc1  25982  efopnlem2  26599  cxpcn3  26691  efrlim  26912  efrlimOLD  26913  precsexlem11  28159  1nns  28281  structvtxval  29001  usgrexmplef  29239  wwlks2onv  29933  elwwlks2ons3im  29934  umgrwwlks2on  29937  konigsberglem4  30234  hhshsslem2  31247  nonbooli  31630  nmopadjlei  32067  cshw1s2  32932  fzto1st  33075  cyc2fv1  33093  cyc3fv1  33109  cyc3fv2  33110  cyc3evpm  33122  1arithidom  33501  zringpid  33516  xrge0iifhmeo  33919  dya2iocbrsiga  34259  dya2icobrsiga  34260  fib0  34383  fib1  34384  coinflippvt  34469  prodfzo03  34587  circlevma  34626  circlemethhgt  34627  hgt750lemg  34638  hgt750lemb  34640  hgt750lema  34641  hgt750leme  34642  tgoldbachgtde  34644  tgoldbachgt  34647  bnj97  34849  bnj553  34881  bnj966  34927  bnj1442  35032  subfacp1lem2a  35160  subfacp1lem5  35164  erdszelem5  35175  erdszelem8  35178  ex-sategoelel12  35407  rankeq1o  36152  0hf  36158  onint1  36430  bj-0eltag  36959  bj-minftyccb  37206  finxpreclem4  37375  fdc  37732  reheibor  37826  0prjspnlem  42604  0prjspnrel  42608  pw2f1ocnv  43019  onexoegt  43226  2omomeqom  43285  omnord1ex  43286  oege2  43289  oenord1ex  43297  oenord1  43298  oaomoencom  43299  oenassex  43300  comptiunov2i  43688  clsk1indlem4  44026  clsk1indlem1  44027  mnuprdlem3  44256  sucidALTVD  44852  sucidALT  44853  sucidVD  44854  wfaxnul  44979  wfaxinf2  44984  nregmodellem  44999  rfcnpre1  45006  eliuniincex  45096  iocopn  45511  icoopn  45516  islptre  45610  cnrefiisplem  45820  icccncfext  45878  fourierdlem103  46200  fourierdlem104  46201  iooborel  46342  upwordnul  46871  upwordsing  46875  sprsymrelfo  47491  sbgoldbo  47781  stgr1  47953  isubgr3stgrlem7  47964  gpg3kgrtriexlem5  48071  pglem  48075  0even  48218  2even  48220  2zrngamgm  48226  zlmodzxzldeplem3  48484  rrx2pxel  48693  rrx2pyel  48694  rrx2linesl  48725  2sphere0  48732  i0oii  48901  io1ii  48902  setc1onsubc  49584