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  5469  opi2  5470  frrlem14  8287  wfrlem14OLD  8325  wfrlem16OLD  8327  seqomlem3  8455  nlim2  8493  oneo  8584  nnneo  8657  0elixp  8926  ac6sfi  9290  tz9.13  9789  rankval  9814  rankid  9831  ssrankr1  9833  rankel  9837  rankval3  9838  rankpw  9841  rankss  9847  ranksn  9852  rankuni2  9853  rankun  9854  rankpr  9855  rankop  9856  rankeq0  9859  rankr1b  9862  djuun  9924  dju1dif  10170  isfin4p1  10313  fin1a2lem4  10401  fin1a2lem6  10403  hsmexlem6  10429  dcomex  10445  axdc3lem4  10451  canthp1lem2  10651  pwxpndom2  10663  rankcf  10775  grutsk  10820  axgroth3  10829  inaprc  10834  1lt2pi  10903  pnfxr  11273  mnfxr  11276  1nn  12228  uzrdg0i  13929  axdc4uzlem  13953  ccat2s1p2  14585  wrdl3s3  14918  infcvgaux1i  15808  0bits  16385  sadcf  16399  prmreclem6  16859  fnpr2ob  17509  setcepi  18043  setc2obas  18049  setc2ohom  18050  cat1  18052  smndex1mnd  18828  smndex1id  18829  pwmnd  18855  grpss  18877  psgnunilem2  19405  psgnprfval2  19433  efgi0  19630  efgi1  19631  vrgpf  19678  vrgpinv  19679  frgpuptinv  19681  frgpup2  19686  frgpnabllem1  19783  dmdprdpr  19961  dprdpr  19962  pzriprnglem7  21257  pzriprnglem13  21263  pzriprng1ALT  21266  m2detleiblem3  22352  m2detleiblem4  22353  m2detleib  22354  leordtval2  22937  xpstopnlem1  23534  xpstopnlem2  23536  ptcmp  23783  tsmsfbas  23853  zcld  24550  sszcld  24554  abscncfALT  24666  iimulcn  24682  iimulcnOLD  24683  icopnfhmeo  24689  iccpnfhmeo  24691  xrhmeo  24692  cnstrcvs  24889  cncvs  24893  dveflem  25729  ftc1  25792  efopnlem2  26398  cxpcn3  26489  efrlim  26707  precsexlem11  27899  0n0s  27936  structvtxval  28545  usgrexmplef  28780  wwlks2onv  29471  elwwlks2ons3im  29472  umgrwwlks2on  29475  konigsberglem4  29772  hhshsslem2  30785  nonbooli  31168  nmopadjlei  31605  cshw1s2  32388  fzto1st  32529  cyc2fv1  32547  cyc3fv1  32563  cyc3fv2  32564  cyc3evpm  32576  xrge0iifhmeo  33211  dya2iocbrsiga  33569  dya2icobrsiga  33570  fib0  33693  fib1  33694  coinflippvt  33778  prodfzo03  33910  circlevma  33949  circlemethhgt  33950  hgt750lemg  33961  hgt750lemb  33963  hgt750lema  33964  hgt750leme  33965  tgoldbachgtde  33967  tgoldbachgt  33970  bnj97  34172  bnj553  34204  bnj966  34250  bnj1442  34355  subfacp1lem2a  34466  subfacp1lem5  34470  erdszelem5  34481  erdszelem8  34484  ex-sategoelel12  34713  rankeq1o  35444  0hf  35450  onint1  35638  bj-0eltag  36163  bj-minftyccb  36410  finxpreclem4  36579  fdc  36917  reheibor  37011  0prjspnlem  41668  0prjspnrel  41672  pw2f1ocnv  42079  onexoegt  42296  2omomeqom  42356  omnord1ex  42357  oege2  42360  oenord1ex  42368  oenord1  42369  oaomoencom  42370  oenassex  42371  comptiunov2i  42760  clsk1indlem4  43098  clsk1indlem1  43099  mnuprdlem3  43336  sucidALTVD  43934  sucidALT  43935  sucidVD  43936  rfcnpre1  44006  eliuniincex  44101  iocopn  44533  icoopn  44538  islptre  44635  cnrefiisplem  44845  icccncfext  44903  fourierdlem103  45225  fourierdlem104  45226  iooborel  45367  upwordnul  45894  upwordsing  45898  sprsymrelfo  46465  sbgoldbo  46755  0even  46919  2even  46921  2zrngamgm  46927  zlmodzxzldeplem3  47272  rrx2pxel  47486  rrx2pyel  47487  rrx2linesl  47518  2sphere0  47525  i0oii  47641  io1ii  47642