Theorem eleqtrri 2833

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 2744	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	eleqtri 2832	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 2707

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

This theorem is referenced by:  3eltr4i  2847  vex  3463  opi1  5443  opi2  5444  frrlem14  8296  wfrlem14OLD  8334  wfrlem16OLD  8336  seqomlem3  8464  nlim2  8500  oneo  8591  nnneo  8665  0elixp  8941  ac6sfi  9290  tz9.13  9803  rankval  9828  rankid  9845  ssrankr1  9847  rankel  9851  rankval3  9852  rankpw  9855  rankss  9861  ranksn  9866  rankuni2  9867  rankun  9868  rankpr  9869  rankop  9870  rankeq0  9873  rankr1b  9876  djuun  9938  dju1dif  10185  isfin4p1  10327  fin1a2lem4  10415  fin1a2lem6  10417  hsmexlem6  10443  dcomex  10459  axdc3lem4  10465  canthp1lem2  10665  pwxpndom2  10677  rankcf  10789  grutsk  10834  axgroth3  10843  inaprc  10848  1lt2pi  10917  pnfxr  11287  mnfxr  11290  1nn  12249  uzrdg0i  13975  axdc4uzlem  13999  ccat2s1p2  14646  wrdl3s3  14979  infcvgaux1i  15871  0bits  16456  sadcf  16470  prmreclem6  16939  fnpr2ob  17570  setcepi  18099  setc2obas  18105  setc2ohom  18106  cat1  18108  smndex1mnd  18886  smndex1id  18887  pwmnd  18913  grpss  18935  psgnunilem2  19474  psgnprfval2  19502  efgi0  19699  efgi1  19700  vrgpf  19747  vrgpinv  19748  frgpuptinv  19750  frgpup2  19755  frgpnabllem1  19852  dmdprdpr  20030  dprdpr  20031  pzriprnglem7  21446  pzriprnglem13  21452  pzriprng1ALT  21455  m2detleiblem3  22565  m2detleiblem4  22566  m2detleib  22567  leordtval2  23148  xpstopnlem1  23745  xpstopnlem2  23747  ptcmp  23994  tsmsfbas  24064  zcld  24751  sszcld  24755  abscncfALT  24867  iimulcn  24883  iimulcnOLD  24884  icopnfhmeo  24890  iccpnfhmeo  24892  xrhmeo  24893  cnstrcvs  25090  cncvs  25094  dveflem  25933  ftc1  25999  efopnlem2  26616  cxpcn3  26708  efrlim  26929  efrlimOLD  26930  precsexlem11  28158  1nns  28269  structvtxval  28946  usgrexmplef  29184  wwlks2onv  29881  elwwlks2ons3im  29882  umgrwwlks2on  29885  konigsberglem4  30182  hhshsslem2  31195  nonbooli  31578  nmopadjlei  32015  cshw1s2  32882  fzto1st  33060  cyc2fv1  33078  cyc3fv1  33094  cyc3fv2  33095  cyc3evpm  33107  1arithidom  33498  zringpid  33513  xrge0iifhmeo  33913  dya2iocbrsiga  34253  dya2icobrsiga  34254  fib0  34377  fib1  34378  coinflippvt  34463  prodfzo03  34581  circlevma  34620  circlemethhgt  34621  hgt750lemg  34632  hgt750lemb  34634  hgt750lema  34635  hgt750leme  34636  tgoldbachgtde  34638  tgoldbachgt  34641  bnj97  34843  bnj553  34875  bnj966  34921  bnj1442  35026  subfacp1lem2a  35148  subfacp1lem5  35152  erdszelem5  35163  erdszelem8  35166  ex-sategoelel12  35395  rankeq1o  36135  0hf  36141  onint1  36413  bj-0eltag  36942  bj-minftyccb  37189  finxpreclem4  37358  fdc  37715  reheibor  37809  0prjspnlem  42593  0prjspnrel  42597  pw2f1ocnv  43008  onexoegt  43215  2omomeqom  43274  omnord1ex  43275  oege2  43278  oenord1ex  43286  oenord1  43287  oaomoencom  43288  oenassex  43289  comptiunov2i  43677  clsk1indlem4  44015  clsk1indlem1  44016  mnuprdlem3  44246  sucidALTVD  44842  sucidALT  44843  sucidVD  44844  wfaxnul  44969  wfaxinf2  44974  rfcnpre1  44991  eliuniincex  45081  iocopn  45497  icoopn  45502  islptre  45596  cnrefiisplem  45806  icccncfext  45864  fourierdlem103  46186  fourierdlem104  46187  iooborel  46328  upwordnul  46857  upwordsing  46861  sprsymrelfo  47459  sbgoldbo  47749  stgr1  47921  isubgr3stgrlem7  47932  gpg3kgrtriexlem5  48037  0even  48160  2even  48162  2zrngamgm  48168  zlmodzxzldeplem3  48426  rrx2pxel  48639  rrx2pyel  48640  rrx2linesl  48671  2sphere0  48678  i0oii  48842  io1ii  48843  setc1onsubc  49427