Theorem eleqtrri 2827

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

Syntax hints:   = wceq 1540   ∈ wcel 2109

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3eltr4i  2841  vex  3451  opi1  5428  opi2  5429  frrlem14  8278  seqomlem3  8420  nlim2  8454  oneo  8545  nnneo  8619  0elixp  8902  ac6sfi  9231  tz9.13  9744  rankval  9769  rankid  9786  ssrankr1  9788  rankel  9792  rankval3  9793  rankpw  9796  rankss  9802  ranksn  9807  rankuni2  9808  rankun  9809  rankpr  9810  rankop  9811  rankeq0  9814  rankr1b  9817  djuun  9879  dju1dif  10126  isfin4p1  10268  fin1a2lem4  10356  fin1a2lem6  10358  hsmexlem6  10384  dcomex  10400  axdc3lem4  10406  canthp1lem2  10606  pwxpndom2  10618  rankcf  10730  grutsk  10775  axgroth3  10784  inaprc  10789  1lt2pi  10858  pnfxr  11228  mnfxr  11231  1nn  12197  uzrdg0i  13924  axdc4uzlem  13948  ccat2s1p2  14595  wrdl3s3  14928  infcvgaux1i  15823  0bits  16409  sadcf  16423  prmreclem6  16892  fnpr2ob  17521  setcepi  18050  setc2obas  18056  setc2ohom  18057  cat1  18059  smndex1mnd  18837  smndex1id  18838  pwmnd  18864  grpss  18886  psgnunilem2  19425  psgnprfval2  19453  efgi0  19650  efgi1  19651  vrgpf  19698  vrgpinv  19699  frgpuptinv  19701  frgpup2  19706  frgpnabllem1  19803  dmdprdpr  19981  dprdpr  19982  pzriprnglem7  21397  pzriprnglem13  21403  pzriprng1ALT  21406  m2detleiblem3  22516  m2detleiblem4  22517  m2detleib  22518  leordtval2  23099  xpstopnlem1  23696  xpstopnlem2  23698  ptcmp  23945  tsmsfbas  24015  zcld  24702  sszcld  24706  abscncfALT  24818  iimulcn  24834  iimulcnOLD  24835  icopnfhmeo  24841  iccpnfhmeo  24843  xrhmeo  24844  cnstrcvs  25041  cncvs  25045  dveflem  25883  ftc1  25949  efopnlem2  26566  cxpcn3  26658  efrlim  26879  efrlimOLD  26880  precsexlem11  28119  1nns  28241  structvtxval  28948  usgrexmplef  29186  wwlks2onv  29883  elwwlks2ons3im  29884  umgrwwlks2on  29887  konigsberglem4  30184  hhshsslem2  31197  nonbooli  31580  nmopadjlei  32017  cshw1s2  32882  fzto1st  33060  cyc2fv1  33078  cyc3fv1  33094  cyc3fv2  33095  cyc3evpm  33107  1arithidom  33508  zringpid  33523  xrge0iifhmeo  33926  dya2iocbrsiga  34266  dya2icobrsiga  34267  fib0  34390  fib1  34391  coinflippvt  34476  prodfzo03  34594  circlevma  34633  circlemethhgt  34634  hgt750lemg  34645  hgt750lemb  34647  hgt750lema  34648  hgt750leme  34649  tgoldbachgtde  34651  tgoldbachgt  34654  bnj97  34856  bnj553  34888  bnj966  34934  bnj1442  35039  subfacp1lem2a  35167  subfacp1lem5  35171  erdszelem5  35182  erdszelem8  35185  ex-sategoelel12  35414  rankeq1o  36159  0hf  36165  onint1  36437  bj-0eltag  36966  bj-minftyccb  37213  finxpreclem4  37382  fdc  37739  reheibor  37833  0prjspnlem  42611  0prjspnrel  42615  pw2f1ocnv  43026  onexoegt  43233  2omomeqom  43292  omnord1ex  43293  oege2  43296  oenord1ex  43304  oenord1  43305  oaomoencom  43306  oenassex  43307  comptiunov2i  43695  clsk1indlem4  44033  clsk1indlem1  44034  mnuprdlem3  44263  sucidALTVD  44859  sucidALT  44860  sucidVD  44861  wfaxnul  44986  wfaxinf2  44991  nregmodellem  45006  rfcnpre1  45013  eliuniincex  45103  iocopn  45518  icoopn  45523  islptre  45617  cnrefiisplem  45827  icccncfext  45885  fourierdlem103  46207  fourierdlem104  46208  iooborel  46349  upwordnul  46878  upwordsing  46882  sprsymrelfo  47498  sbgoldbo  47788  stgr1  47960  isubgr3stgrlem7  47971  gpg3kgrtriexlem5  48078  pglem  48082  0even  48225  2even  48227  2zrngamgm  48233  zlmodzxzldeplem3  48491  rrx2pxel  48700  rrx2pyel  48701  rrx2linesl  48732  2sphere0  48739  i0oii  48908  io1ii  48909  setc1onsubc  49591