Theorem eleqtrri 2837

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

Syntax hints:   = wceq 1536   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-clel 2813

This theorem is referenced by:  3eltr4i  2851  vex  3481  opi1  5478  opi2  5479  frrlem14  8322  wfrlem14OLD  8360  wfrlem16OLD  8362  seqomlem3  8490  nlim2  8526  oneo  8617  nnneo  8691  0elixp  8967  ac6sfi  9317  tz9.13  9828  rankval  9853  rankid  9870  ssrankr1  9872  rankel  9876  rankval3  9877  rankpw  9880  rankss  9886  ranksn  9891  rankuni2  9892  rankun  9893  rankpr  9894  rankop  9895  rankeq0  9898  rankr1b  9901  djuun  9963  dju1dif  10210  isfin4p1  10352  fin1a2lem4  10440  fin1a2lem6  10442  hsmexlem6  10468  dcomex  10484  axdc3lem4  10490  canthp1lem2  10690  pwxpndom2  10702  rankcf  10814  grutsk  10859  axgroth3  10868  inaprc  10873  1lt2pi  10942  pnfxr  11312  mnfxr  11315  1nn  12274  uzrdg0i  13996  axdc4uzlem  14020  ccat2s1p2  14664  wrdl3s3  14997  infcvgaux1i  15889  0bits  16472  sadcf  16486  prmreclem6  16954  fnpr2ob  17604  setcepi  18141  setc2obas  18147  setc2ohom  18148  cat1  18150  smndex1mnd  18935  smndex1id  18936  pwmnd  18962  grpss  18984  psgnunilem2  19527  psgnprfval2  19555  efgi0  19752  efgi1  19753  vrgpf  19800  vrgpinv  19801  frgpuptinv  19803  frgpup2  19808  frgpnabllem1  19905  dmdprdpr  20083  dprdpr  20084  pzriprnglem7  21515  pzriprnglem13  21521  pzriprng1ALT  21524  m2detleiblem3  22650  m2detleiblem4  22651  m2detleib  22652  leordtval2  23235  xpstopnlem1  23832  xpstopnlem2  23834  ptcmp  24081  tsmsfbas  24151  zcld  24848  sszcld  24852  abscncfALT  24964  iimulcn  24980  iimulcnOLD  24981  icopnfhmeo  24987  iccpnfhmeo  24989  xrhmeo  24990  cnstrcvs  25187  cncvs  25191  dveflem  26031  ftc1  26097  efopnlem2  26713  cxpcn3  26805  efrlim  27026  efrlimOLD  27027  precsexlem11  28255  1nns  28366  structvtxval  29052  usgrexmplef  29290  wwlks2onv  29982  elwwlks2ons3im  29983  umgrwwlks2on  29986  konigsberglem4  30283  hhshsslem2  31296  nonbooli  31679  nmopadjlei  32116  cshw1s2  32929  fzto1st  33105  cyc2fv1  33123  cyc3fv1  33139  cyc3fv2  33140  cyc3evpm  33152  1arithidom  33544  zringpid  33559  xrge0iifhmeo  33896  dya2iocbrsiga  34256  dya2icobrsiga  34257  fib0  34380  fib1  34381  coinflippvt  34465  prodfzo03  34596  circlevma  34635  circlemethhgt  34636  hgt750lemg  34647  hgt750lemb  34649  hgt750lema  34650  hgt750leme  34651  tgoldbachgtde  34653  tgoldbachgt  34656  bnj97  34858  bnj553  34890  bnj966  34936  bnj1442  35041  subfacp1lem2a  35164  subfacp1lem5  35168  erdszelem5  35179  erdszelem8  35182  ex-sategoelel12  35411  rankeq1o  36152  0hf  36158  onint1  36431  bj-0eltag  36960  bj-minftyccb  37207  finxpreclem4  37376  fdc  37731  reheibor  37825  0prjspnlem  42609  0prjspnrel  42613  pw2f1ocnv  43025  onexoegt  43232  2omomeqom  43292  omnord1ex  43293  oege2  43296  oenord1ex  43304  oenord1  43305  oaomoencom  43306  oenassex  43307  comptiunov2i  43695  clsk1indlem4  44033  clsk1indlem1  44034  mnuprdlem3  44269  sucidALTVD  44867  sucidALT  44868  sucidVD  44869  rfcnpre1  44956  eliuniincex  45048  iocopn  45472  icoopn  45477  islptre  45574  cnrefiisplem  45784  icccncfext  45842  fourierdlem103  46164  fourierdlem104  46165  iooborel  46306  upwordnul  46833  upwordsing  46837  sprsymrelfo  47421  sbgoldbo  47711  stgr1  47863  isubgr3stgrlem7  47874  0even  48080  2even  48082  2zrngamgm  48088  zlmodzxzldeplem3  48347  rrx2pxel  48560  rrx2pyel  48561  rrx2linesl  48592  2sphere0  48599  i0oii  48715  io1ii  48716