Theorem eleqtrri 2839

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

Syntax hints:   = wceq 1539   ∈ wcel 2107

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-ex 1783  df-cleq 2731  df-clel 2817

This theorem is referenced by:  3eltr4i  2853  vex  3437  vexOLD  3438  opi1  5384  opi2  5385  frrlem14  8124  wfrlem14OLD  8162  wfrlem16OLD  8164  seqomlem3  8292  nlim2  8329  oneo  8421  nnneo  8494  0elixp  8726  ac6sfi  9067  tz9.13  9558  rankval  9583  rankid  9600  ssrankr1  9602  rankel  9606  rankval3  9607  rankpw  9610  rankss  9616  ranksn  9621  rankuni2  9622  rankun  9623  rankpr  9624  rankop  9625  rankeq0  9628  rankr1b  9631  djuun  9693  dju1dif  9937  isfin4p1  10080  fin1a2lem4  10168  fin1a2lem6  10170  hsmexlem6  10196  dcomex  10212  axdc3lem4  10218  canthp1lem2  10418  pwxpndom2  10430  rankcf  10542  grutsk  10587  axgroth3  10596  inaprc  10601  1lt2pi  10670  pnfxr  11038  mnfxr  11041  1nn  11993  uzrdg0i  13688  axdc4uzlem  13712  ccat2s1p2  14346  ccat2s1p2OLD  14348  wrdl3s3  14686  infcvgaux1i  15578  0bits  16155  sadcf  16169  prmreclem6  16631  fnpr2ob  17278  setcepi  17812  setc2obas  17818  setc2ohom  17819  cat1  17821  smndex1mnd  18558  smndex1id  18559  pwmnd  18585  grpss  18606  psgnunilem2  19112  psgnprfval2  19140  efgi0  19335  efgi1  19336  vrgpf  19383  vrgpinv  19384  frgpuptinv  19386  frgpup2  19391  frgpnabllem1  19483  dmdprdpr  19661  dprdpr  19662  m2detleiblem3  21787  m2detleiblem4  21788  m2detleib  21789  leordtval2  22372  xpstopnlem1  22969  xpstopnlem2  22971  ptcmp  23218  tsmsfbas  23288  zcld  23985  sszcld  23989  abscncfALT  24096  iimulcn  24110  icopnfhmeo  24115  iccpnfhmeo  24117  xrhmeo  24118  cnstrcvs  24313  cncvs  24317  dveflem  25152  ftc1  25215  efopnlem2  25821  cxpcn3  25910  efrlim  26128  structvtxval  27400  usgrexmplef  27635  wwlks2onv  28327  elwwlks2ons3im  28328  umgrwwlks2on  28331  konigsberglem4  28628  hhshsslem2  29639  nonbooli  30022  nmopadjlei  30459  cshw1s2  31241  fzto1st  31379  cyc2fv1  31397  cyc3fv1  31413  cyc3fv2  31414  cyc3evpm  31426  xrge0iifhmeo  31895  dya2iocbrsiga  32251  dya2icobrsiga  32252  fib0  32375  fib1  32376  coinflippvt  32460  prodfzo03  32592  circlevma  32631  circlemethhgt  32632  hgt750lemg  32643  hgt750lemb  32645  hgt750lema  32646  hgt750leme  32647  tgoldbachgtde  32649  tgoldbachgt  32652  bnj97  32855  bnj553  32887  bnj966  32933  bnj1442  33038  subfacp1lem2a  33151  subfacp1lem5  33155  erdszelem5  33166  erdszelem8  33169  ex-sategoelel12  33398  rankeq1o  34482  0hf  34488  onint1  34647  bj-0eltag  35177  bj-minftyccb  35405  finxpreclem4  35574  fdc  35912  reheibor  36006  0prjspnlem  40467  0prjspnrel  40471  pw2f1ocnv  40866  comptiunov2i  41321  clsk1indlem4  41661  clsk1indlem1  41662  mnuprdlem3  41899  sucidALTVD  42497  sucidALT  42498  sucidVD  42499  rfcnpre1  42569  eliuniincex  42666  iocopn  43065  icoopn  43070  islptre  43167  cnrefiisplem  43377  icccncfext  43435  fourierdlem103  43757  fourierdlem104  43758  iooborel  43897  sprsymrelfo  44960  sbgoldbo  45250  0even  45500  2even  45502  2zrngamgm  45508  zlmodzxzldeplem3  45854  rrx2pxel  46068  rrx2pyel  46069  rrx2linesl  46100  2sphere0  46107  i0oii  46224  io1ii  46225  upwordnul  46526  upwordsing  46530