Theorem eleqtrri 2840

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 2839	1 ⊢ 𝐴 ∈ 𝐶

Syntax hints:   = wceq 1540   ∈ wcel 2108

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  3eltr4i  2854  vex  3484  opi1  5473  opi2  5474  frrlem14  8324  wfrlem14OLD  8362  wfrlem16OLD  8364  seqomlem3  8492  nlim2  8528  oneo  8619  nnneo  8693  0elixp  8969  ac6sfi  9320  tz9.13  9831  rankval  9856  rankid  9873  ssrankr1  9875  rankel  9879  rankval3  9880  rankpw  9883  rankss  9889  ranksn  9894  rankuni2  9895  rankun  9896  rankpr  9897  rankop  9898  rankeq0  9901  rankr1b  9904  djuun  9966  dju1dif  10213  isfin4p1  10355  fin1a2lem4  10443  fin1a2lem6  10445  hsmexlem6  10471  dcomex  10487  axdc3lem4  10493  canthp1lem2  10693  pwxpndom2  10705  rankcf  10817  grutsk  10862  axgroth3  10871  inaprc  10876  1lt2pi  10945  pnfxr  11315  mnfxr  11318  1nn  12277  uzrdg0i  14000  axdc4uzlem  14024  ccat2s1p2  14668  wrdl3s3  15001  infcvgaux1i  15893  0bits  16476  sadcf  16490  prmreclem6  16959  fnpr2ob  17603  setcepi  18133  setc2obas  18139  setc2ohom  18140  cat1  18142  smndex1mnd  18923  smndex1id  18924  pwmnd  18950  grpss  18972  psgnunilem2  19513  psgnprfval2  19541  efgi0  19738  efgi1  19739  vrgpf  19786  vrgpinv  19787  frgpuptinv  19789  frgpup2  19794  frgpnabllem1  19891  dmdprdpr  20069  dprdpr  20070  pzriprnglem7  21498  pzriprnglem13  21504  pzriprng1ALT  21507  m2detleiblem3  22635  m2detleiblem4  22636  m2detleib  22637  leordtval2  23220  xpstopnlem1  23817  xpstopnlem2  23819  ptcmp  24066  tsmsfbas  24136  zcld  24835  sszcld  24839  abscncfALT  24951  iimulcn  24967  iimulcnOLD  24968  icopnfhmeo  24974  iccpnfhmeo  24976  xrhmeo  24977  cnstrcvs  25174  cncvs  25178  dveflem  26017  ftc1  26083  efopnlem2  26699  cxpcn3  26791  efrlim  27012  efrlimOLD  27013  precsexlem11  28241  1nns  28352  structvtxval  29038  usgrexmplef  29276  wwlks2onv  29973  elwwlks2ons3im  29974  umgrwwlks2on  29977  konigsberglem4  30274  hhshsslem2  31287  nonbooli  31670  nmopadjlei  32107  cshw1s2  32945  fzto1st  33123  cyc2fv1  33141  cyc3fv1  33157  cyc3fv2  33158  cyc3evpm  33170  1arithidom  33565  zringpid  33580  xrge0iifhmeo  33935  dya2iocbrsiga  34277  dya2icobrsiga  34278  fib0  34401  fib1  34402  coinflippvt  34487  prodfzo03  34618  circlevma  34657  circlemethhgt  34658  hgt750lemg  34669  hgt750lemb  34671  hgt750lema  34672  hgt750leme  34673  tgoldbachgtde  34675  tgoldbachgt  34678  bnj97  34880  bnj553  34912  bnj966  34958  bnj1442  35063  subfacp1lem2a  35185  subfacp1lem5  35189  erdszelem5  35200  erdszelem8  35203  ex-sategoelel12  35432  rankeq1o  36172  0hf  36178  onint1  36450  bj-0eltag  36979  bj-minftyccb  37226  finxpreclem4  37395  fdc  37752  reheibor  37846  0prjspnlem  42633  0prjspnrel  42637  pw2f1ocnv  43049  onexoegt  43256  2omomeqom  43316  omnord1ex  43317  oege2  43320  oenord1ex  43328  oenord1  43329  oaomoencom  43330  oenassex  43331  comptiunov2i  43719  clsk1indlem4  44057  clsk1indlem1  44058  mnuprdlem3  44293  sucidALTVD  44890  sucidALT  44891  sucidVD  44892  wfaxnul  45013  wfaxinf2  45018  rfcnpre1  45024  eliuniincex  45114  iocopn  45533  icoopn  45538  islptre  45634  cnrefiisplem  45844  icccncfext  45902  fourierdlem103  46224  fourierdlem104  46225  iooborel  46366  upwordnul  46895  upwordsing  46899  sprsymrelfo  47484  sbgoldbo  47774  stgr1  47928  isubgr3stgrlem7  47939  gpg3kgrtriexlem5  48043  0even  48153  2even  48155  2zrngamgm  48161  zlmodzxzldeplem3  48419  rrx2pxel  48632  rrx2pyel  48633  rrx2linesl  48664  2sphere0  48671  i0oii  48817  io1ii  48818