Theorem eleqtrri 2831

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

Syntax hints:   = wceq 1540   ∈ wcel 2105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-ex 1781  df-cleq 2723  df-clel 2809

This theorem is referenced by:  3eltr4i  2845  vex  3477  vexOLD  3478  opi1  5468  opi2  5469  frrlem14  8290  wfrlem14OLD  8328  wfrlem16OLD  8330  seqomlem3  8458  nlim2  8496  oneo  8587  nnneo  8660  0elixp  8929  ac6sfi  9293  tz9.13  9792  rankval  9817  rankid  9834  ssrankr1  9836  rankel  9840  rankval3  9841  rankpw  9844  rankss  9850  ranksn  9855  rankuni2  9856  rankun  9857  rankpr  9858  rankop  9859  rankeq0  9862  rankr1b  9865  djuun  9927  dju1dif  10173  isfin4p1  10316  fin1a2lem4  10404  fin1a2lem6  10406  hsmexlem6  10432  dcomex  10448  axdc3lem4  10454  canthp1lem2  10654  pwxpndom2  10666  rankcf  10778  grutsk  10823  axgroth3  10832  inaprc  10837  1lt2pi  10906  pnfxr  11275  mnfxr  11278  1nn  12230  uzrdg0i  13931  axdc4uzlem  13955  ccat2s1p2  14587  wrdl3s3  14920  infcvgaux1i  15810  0bits  16387  sadcf  16401  prmreclem6  16861  fnpr2ob  17511  setcepi  18048  setc2obas  18054  setc2ohom  18055  cat1  18057  smndex1mnd  18833  smndex1id  18834  pwmnd  18860  grpss  18882  psgnunilem2  19411  psgnprfval2  19439  efgi0  19636  efgi1  19637  vrgpf  19684  vrgpinv  19685  frgpuptinv  19687  frgpup2  19692  frgpnabllem1  19789  dmdprdpr  19967  dprdpr  19968  pzriprnglem7  21347  pzriprnglem13  21353  pzriprng1ALT  21356  m2detleiblem3  22451  m2detleiblem4  22452  m2detleib  22453  leordtval2  23036  xpstopnlem1  23633  xpstopnlem2  23635  ptcmp  23882  tsmsfbas  23952  zcld  24649  sszcld  24653  abscncfALT  24765  iimulcn  24781  iimulcnOLD  24782  icopnfhmeo  24788  iccpnfhmeo  24790  xrhmeo  24791  cnstrcvs  24988  cncvs  24992  dveflem  25831  ftc1  25897  efopnlem2  26505  cxpcn3  26597  efrlim  26815  precsexlem11  28028  0n0s  28083  1nns  28099  structvtxval  28714  usgrexmplef  28949  wwlks2onv  29640  elwwlks2ons3im  29641  umgrwwlks2on  29644  konigsberglem4  29941  hhshsslem2  30954  nonbooli  31337  nmopadjlei  31774  cshw1s2  32557  fzto1st  32698  cyc2fv1  32716  cyc3fv1  32732  cyc3fv2  32733  cyc3evpm  32745  xrge0iifhmeo  33380  dya2iocbrsiga  33738  dya2icobrsiga  33739  fib0  33862  fib1  33863  coinflippvt  33947  prodfzo03  34079  circlevma  34118  circlemethhgt  34119  hgt750lemg  34130  hgt750lemb  34132  hgt750lema  34133  hgt750leme  34134  tgoldbachgtde  34136  tgoldbachgt  34139  bnj97  34341  bnj553  34373  bnj966  34419  bnj1442  34524  subfacp1lem2a  34635  subfacp1lem5  34639  erdszelem5  34650  erdszelem8  34653  ex-sategoelel12  34882  rankeq1o  35613  0hf  35619  onint1  35798  bj-0eltag  36323  bj-minftyccb  36570  finxpreclem4  36739  fdc  37077  reheibor  37171  0prjspnlem  41828  0prjspnrel  41832  pw2f1ocnv  42239  onexoegt  42456  2omomeqom  42516  omnord1ex  42517  oege2  42520  oenord1ex  42528  oenord1  42529  oaomoencom  42530  oenassex  42531  comptiunov2i  42920  clsk1indlem4  43258  clsk1indlem1  43259  mnuprdlem3  43496  sucidALTVD  44094  sucidALT  44095  sucidVD  44096  rfcnpre1  44166  eliuniincex  44260  iocopn  44692  icoopn  44697  islptre  44794  cnrefiisplem  45004  icccncfext  45062  fourierdlem103  45384  fourierdlem104  45385  iooborel  45526  upwordnul  46053  upwordsing  46057  sprsymrelfo  46624  sbgoldbo  46914  0even  47074  2even  47076  2zrngamgm  47082  zlmodzxzldeplem3  47345  rrx2pxel  47559  rrx2pyel  47560  rrx2linesl  47591  2sphere0  47598  i0oii  47714  io1ii  47715