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

Syntax hints:   = wceq 1541   ∈ wcel 2113

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 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

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

This theorem is referenced by:  3eltr4i  2847  vex  3442  opi1  5414  opi2  5415  frrlem14  8239  seqomlem3  8381  nlim2  8415  oneo  8506  nnneo  8581  0elixp  8865  ac6sfi  9182  tz9.13  9701  rankval  9726  rankid  9743  ssrankr1  9745  rankel  9749  rankval3  9750  rankpw  9753  rankss  9759  ranksn  9764  rankuni2  9765  rankun  9766  rankpr  9767  rankop  9768  rankeq0  9771  rankr1b  9774  djuun  9836  dju1dif  10081  isfin4p1  10223  fin1a2lem4  10311  fin1a2lem6  10313  hsmexlem6  10339  dcomex  10355  axdc3lem4  10361  canthp1lem2  10562  pwxpndom2  10574  rankcf  10686  grutsk  10731  axgroth3  10740  inaprc  10745  1lt2pi  10814  pnfxr  11184  mnfxr  11187  1nn  12154  uzrdg0i  13880  axdc4uzlem  13904  ccat2s1p2  14552  wrdl3s3  14883  infcvgaux1i  15778  0bits  16364  sadcf  16378  prmreclem6  16847  fnpr2ob  17477  setcepi  18010  setc2obas  18016  setc2ohom  18017  cat1  18019  smndex1mnd  18833  smndex1id  18834  pwmnd  18860  grpss  18882  psgnunilem2  19422  psgnprfval2  19450  efgi0  19647  efgi1  19648  vrgpf  19695  vrgpinv  19696  frgpuptinv  19698  frgpup2  19703  frgpnabllem1  19800  dmdprdpr  19978  dprdpr  19979  pzriprnglem7  21440  pzriprnglem13  21446  pzriprng1ALT  21449  m2detleiblem3  22571  m2detleiblem4  22572  m2detleib  22573  leordtval2  23154  xpstopnlem1  23751  xpstopnlem2  23753  ptcmp  24000  tsmsfbas  24070  zcld  24756  sszcld  24760  abscncfALT  24872  iimulcn  24888  iimulcnOLD  24889  icopnfhmeo  24895  iccpnfhmeo  24897  xrhmeo  24898  cnstrcvs  25095  cncvs  25099  dveflem  25937  ftc1  26003  efopnlem2  26620  cxpcn3  26712  efrlim  26933  efrlimOLD  26934  precsexlem11  28185  1nns  28309  structvtxval  29043  usgrexmplef  29281  wwlks2onv  29975  elwwlks2ons3im  29976  usgrwwlks2on  29980  umgrwwlks2on  29981  konigsberglem4  30279  hhshsslem2  31292  nonbooli  31675  nmopadjlei  32112  cshw1s2  32991  fzto1st  33134  cyc2fv1  33152  cyc3fv1  33168  cyc3fv2  33169  cyc3evpm  33181  1arithidom  33567  zringpid  33582  vieta  33685  xrge0iifhmeo  34042  dya2iocbrsiga  34381  dya2icobrsiga  34382  fib0  34505  fib1  34506  coinflippvt  34591  prodfzo03  34709  circlevma  34748  circlemethhgt  34749  hgt750lemg  34760  hgt750lemb  34762  hgt750lema  34763  hgt750leme  34764  tgoldbachgtde  34766  tgoldbachgt  34769  bnj97  34971  bnj553  35003  bnj966  35049  bnj1442  35154  fineqvnttrclse  35229  fineqvinfep  35230  subfacp1lem2a  35323  subfacp1lem5  35327  erdszelem5  35338  erdszelem8  35341  ex-sategoelel12  35570  rankeq1o  36314  0hf  36320  onint1  36592  bj-0eltag  37122  bj-minftyccb  37369  finxpreclem4  37538  fdc  37885  reheibor  37979  0prjspnlem  42808  0prjspnrel  42812  pw2f1ocnv  43221  onexoegt  43428  2omomeqom  43487  omnord1ex  43488  oege2  43491  oenord1ex  43499  oenord1  43500  oaomoencom  43501  oenassex  43502  comptiunov2i  43889  clsk1indlem4  44227  clsk1indlem1  44228  mnuprdlem3  44457  sucidALTVD  45052  sucidALT  45053  sucidVD  45054  wfaxnul  45179  wfaxinf2  45184  nregmodellem  45199  rfcnpre1  45206  eliuniincex  45295  iocopn  45708  icoopn  45713  islptre  45807  cnrefiisplem  46015  icccncfext  46073  fourierdlem103  46395  fourierdlem104  46396  iooborel  46537  sprsymrelfo  47685  sbgoldbo  47975  stgr1  48149  isubgr3stgrlem7  48160  gpg3kgrtriexlem5  48275  pglem  48279  grlimedgnedg  48319  0even  48425  2even  48427  2zrngamgm  48433  zlmodzxzldeplem3  48690  rrx2pxel  48899  rrx2pyel  48900  rrx2linesl  48931  2sphere0  48938  i0oii  49107  io1ii  49108  setc1onsubc  49789