Theorem eleqtrri 2889

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

Syntax hints:   = wceq 1538   ∈ wcel 2111

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2791  df-clel 2870

This theorem is referenced by:  3eltr4i  2903  vex  3444  opi1  5325  opi2  5326  wfrlem14  7951  wfrlem16  7953  seqomlem3  8071  oneo  8190  nnneo  8261  0elixp  8476  ac6sfi  8746  tz9.13  9204  rankval  9229  rankid  9246  ssrankr1  9248  rankel  9252  rankval3  9253  rankpw  9256  rankss  9262  ranksn  9267  rankuni2  9268  rankun  9269  rankpr  9270  rankop  9271  rankeq0  9274  rankr1b  9277  djuun  9339  dju1dif  9583  isfin4p1  9726  fin1a2lem4  9814  fin1a2lem6  9816  hsmexlem6  9842  dcomex  9858  axdc3lem4  9864  canthp1lem2  10064  pwxpndom2  10076  rankcf  10188  grutsk  10233  axgroth3  10242  inaprc  10247  1lt2pi  10316  pnfxr  10684  mnfxr  10687  1nn  11636  uzrdg0i  13322  axdc4uzlem  13346  ccat2s1p2  13977  ccat2s1p2OLD  13979  wrdl3s3  14317  infcvgaux1i  15204  0bits  15778  sadcf  15792  prmreclem6  16247  fnpr2ob  16823  setcepi  17340  smndex1mnd  18067  smndex1id  18068  pwmnd  18094  grpss  18113  psgnunilem2  18615  psgnprfval2  18643  efgi0  18838  efgi1  18839  vrgpf  18886  vrgpinv  18887  frgpuptinv  18889  frgpup2  18894  frgpnabllem1  18986  dmdprdpr  19164  dprdpr  19165  m2detleiblem3  21234  m2detleiblem4  21235  m2detleib  21236  leordtval2  21817  xpstopnlem1  22414  xpstopnlem2  22416  ptcmp  22663  tsmsfbas  22733  zcld  23418  sszcld  23422  abscncfALT  23529  iimulcn  23543  icopnfhmeo  23548  iccpnfhmeo  23550  xrhmeo  23551  cnstrcvs  23746  cncvs  23750  dveflem  24582  ftc1  24645  efopnlem2  25248  cxpcn3  25337  efrlim  25555  structvtxval  26814  usgrexmplef  27049  wwlks2onv  27739  elwwlks2ons3im  27740  umgrwwlks2on  27743  konigsberglem4  28040  hhshsslem2  29051  nonbooli  29434  nmopadjlei  29871  cshw1s2  30660  fzto1st  30795  cyc2fv1  30813  cyc3fv1  30829  cyc3fv2  30830  cyc3evpm  30842  xrge0iifhmeo  31289  dya2iocbrsiga  31643  dya2icobrsiga  31644  fib0  31767  fib1  31768  coinflippvt  31852  prodfzo03  31984  circlevma  32023  circlemethhgt  32024  hgt750lemg  32035  hgt750lemb  32037  hgt750lema  32038  hgt750leme  32039  tgoldbachgtde  32041  tgoldbachgt  32044  bnj97  32248  bnj553  32280  bnj966  32326  bnj1442  32431  subfacp1lem2a  32540  subfacp1lem5  32544  erdszelem5  32555  erdszelem8  32558  ex-sategoelel12  32787  frrlem14  33249  rankeq1o  33745  0hf  33751  onint1  33910  bj-0eltag  34414  bj-minftyccb  34640  finxpreclem4  34811  fdc  35183  reheibor  35277  0prjspnlem  39612  0prjspnrel  39613  pw2f1ocnv  39978  comptiunov2i  40407  clsk1indlem4  40747  clsk1indlem1  40748  mnuprdlem3  40982  sucidALTVD  41576  sucidALT  41577  sucidVD  41578  rfcnpre1  41648  eliuniincex  41745  iocopn  42157  icoopn  42162  islptre  42261  cnrefiisplem  42471  icccncfext  42529  fourierdlem103  42851  fourierdlem104  42852  iooborel  42991  sprsymrelfo  44014  sbgoldbo  44305  0even  44555  2even  44557  2zrngamgm  44563  zlmodzxzldeplem3  44911  rrx2pxel  45125  rrx2pyel  45126  rrx2linesl  45157  2sphere0  45164