Theorem eleqtrri 2859

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

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2145

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-clel 2835

This theorem is used by:  3eltr4i  2873  vex  3454  opi1  5444  opi2  5445  frrlem14  8299  seqomlem3  8442  nlim2  8478  oneo  8569  nnneo  8644  0elixp  8937  ac6sfi  9255  tz9.13  9774  rankval  9799  rankid  9816  ssrankr1  9818  rankel  9822  rankval3  9823  rankpw  9826  rankss  9832  ranksn  9837  rankuni2  9838  rankun  9839  rankpr  9840  rankop  9841  rankeq0  9844  rankr1b  9847  djuun  9932  dju1dif  10176  isfin4p1  10318  fin1a2lem4  10406  fin1a2lem6  10408  hsmexlem6  10434  dcomex  10450  axdc3lem4  10456  canthp1lem2  10663  pwxpndom2  10675  rankcf  10787  grutsk  10832  axgroth3  10841  inaprc  10846  1lt2pi  10915  pnfxr  11288  mnfxr  11291  1nn  12269  uzrdg0i  14024  axdc4uzlem  14048  ccat2s1p2  14699  s3rex  15022  wrdl3s3  15036  infcvgaux1i  15947  0bits  16530  sadcf  16544  prmreclem6  17014  fnpr2ob  17645  setcepi  18178  setc2obas  18184  setc2ohom  18185  cat1  18187  smndex1mnd  19023  smndex1id  19024  pwmnd  19057  grpss  19079  psgnunilem2  19623  psgnprfval2  19651  efgi0  19848  efgi1  19849  vrgpf  19896  vrgpinv  19897  frgpuptinv  19899  frgpup2  19904  frgpnabllem1  20001  dmdprdpr  20179  dprdpr  20180  pzriprnglem7  21701  pzriprnglem13  21707  pzriprng1ALT  21710  m2detleiblem3  22852  m2detleiblem4  22853  m2detleib  22854  leordtval2  23438  xpstopnlem1  24036  xpstopnlem2  24038  ptcmp  24285  tsmsfbas  24355  zcld  25041  sszcld  25045  abscncfALT  25153  iimulcn  25167  icopnfhmeo  25172  iccpnfhmeo  25174  xrhmeo  25175  cnstrcvs  25370  cncvs  25374  dveflem  26207  ftc1  26270  efopnlem2  26895  cxpcn3  26986  efrlim  27207  precsexlem11  28483  1nns  28615  structvtxval  29479  usgrexmplef  29720  wwlks2onv  30422  elwwlks2ons3im  30423  usgrwwlks2on  30427  umgrwwlks2on  30428  konigsberglem4  30736  hhshsslem2  31750  nonbooli  32133  nmopadjlei  32570  cshw1s2  33401  fzto1st  33544  cyc2fv1  33562  cyc3fv1  33578  cyc3fv2  33579  cyc3evpm  33591  1arithidom  33948  zringpid  33963  vieta  34091  xrge0iifhmeo  34447  dya2iocbrsiga  34787  dya2icobrsiga  34788  fib0  34911  fib1  34912  coinflippvt  34997  prodfzo03  35112  circlevma  35151  circlemethhgt  35152  hgt750lemg  35163  hgt750lemb  35165  hgt750lema  35166  hgt750leme  35167  tgoldbachgtde  35169  tgoldbachgt  35172  bnj97  35376  bnj553  35408  bnj966  35454  bnj1442  35559  fineqvnttrclse  35651  fineqvinfep  35652  subfacp1lem2a  35760  subfacp1lem5  35764  erdszelem5  35775  erdszelem8  35778  ex-sategoelel12  36007  rankeq1o  36752  0hf  36758  onint1  37069  regsfromunir1  37160  bj-0eltag  37723  bj-minftyccb  37978  finxpreclem4  38149  fdc  38496  reheibor  38590  0prjspnlem  43470  0prjspnrel  43474  pw2f1ocnv  43879  onexoegt  44086  2omomeqom  44145  omnord1ex  44146  oege2  44149  oenord1ex  44157  oenord1  44158  oaomoencom  44159  oenassex  44160  comptiunov2i  44547  clsk1indlem4  44885  clsk1indlem1  44886  mnuprdlem3  45099  sucidALTVD  45693  sucidALT  45694  sucidVD  45695  wfaxnul  45820  wfaxinf2  45825  nregmodellem  45840  rfcnpre1  45854  eliuniincex  45942  iocopn  46351  icoopn  46356  islptre  46450  cnrefiisplem  46658  icccncfext  46716  fourierdlem103  47038  fourierdlem104  47039  iooborel  47180  tannpoly  47759  sprsymrelfo  48398  sbgoldbo  48704  stgr1  48878  isubgr3stgrlem7  48889  gpg3kgrtriexlem5  49004  pglem  49008  grlimedgnedg  49048  0even  49153  2even  49155  2zrngamgm  49161  zlmodzxzldeplem3  49433  rrx2pxel  49642  rrx2pyel  49643  rrx2linesl  49674  2sphere0  49681  i0oii  49847  io1ii  49848  setc1onsubc  50529