Theorem eleqtrri 2835

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

Syntax hints:   = wceq 1542   ∈ wcel 2114

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-clel 2811

This theorem is referenced by:  3eltr4i  2849  vex  3433  opi1  5421  opi2  5422  frrlem14  8249  seqomlem3  8391  nlim2  8425  oneo  8516  nnneo  8591  0elixp  8877  ac6sfi  9194  tz9.13  9715  rankval  9740  rankid  9757  ssrankr1  9759  rankel  9763  rankval3  9764  rankpw  9767  rankss  9773  ranksn  9778  rankuni2  9779  rankun  9780  rankpr  9781  rankop  9782  rankeq0  9785  rankr1b  9788  djuun  9850  dju1dif  10095  isfin4p1  10237  fin1a2lem4  10325  fin1a2lem6  10327  hsmexlem6  10353  dcomex  10369  axdc3lem4  10375  canthp1lem2  10576  pwxpndom2  10588  rankcf  10700  grutsk  10745  axgroth3  10754  inaprc  10759  1lt2pi  10828  pnfxr  11199  mnfxr  11202  1nn  12185  uzrdg0i  13921  axdc4uzlem  13945  ccat2s1p2  14593  wrdl3s3  14924  infcvgaux1i  15822  0bits  16408  sadcf  16422  prmreclem6  16892  fnpr2ob  17522  setcepi  18055  setc2obas  18061  setc2ohom  18062  cat1  18064  smndex1mnd  18881  smndex1id  18882  pwmnd  18908  grpss  18930  psgnunilem2  19470  psgnprfval2  19498  efgi0  19695  efgi1  19696  vrgpf  19743  vrgpinv  19744  frgpuptinv  19746  frgpup2  19751  frgpnabllem1  19848  dmdprdpr  20026  dprdpr  20027  pzriprnglem7  21467  pzriprnglem13  21473  pzriprng1ALT  21476  m2detleiblem3  22594  m2detleiblem4  22595  m2detleib  22596  leordtval2  23177  xpstopnlem1  23774  xpstopnlem2  23776  ptcmp  24023  tsmsfbas  24093  zcld  24779  sszcld  24783  abscncfALT  24891  iimulcn  24905  icopnfhmeo  24910  iccpnfhmeo  24912  xrhmeo  24913  cnstrcvs  25108  cncvs  25112  dveflem  25946  ftc1  26009  efopnlem2  26621  cxpcn3  26712  efrlim  26933  precsexlem11  28209  1nns  28341  structvtxval  29090  usgrexmplef  29328  wwlks2onv  30021  elwwlks2ons3im  30022  usgrwwlks2on  30026  umgrwwlks2on  30027  konigsberglem4  30325  hhshsslem2  31339  nonbooli  31722  nmopadjlei  32159  cshw1s2  33020  fzto1st  33164  cyc2fv1  33182  cyc3fv1  33198  cyc3fv2  33199  cyc3evpm  33211  1arithidom  33597  zringpid  33612  vieta  33724  xrge0iifhmeo  34080  dya2iocbrsiga  34419  dya2icobrsiga  34420  fib0  34543  fib1  34544  coinflippvt  34629  prodfzo03  34747  circlevma  34786  circlemethhgt  34787  hgt750lemg  34798  hgt750lemb  34800  hgt750lema  34801  hgt750leme  34802  tgoldbachgtde  34804  tgoldbachgt  34807  bnj97  35008  bnj553  35040  bnj966  35086  bnj1442  35191  fineqvnttrclse  35268  fineqvinfep  35269  subfacp1lem2a  35362  subfacp1lem5  35366  erdszelem5  35377  erdszelem8  35380  ex-sategoelel12  35609  rankeq1o  36353  0hf  36359  onint1  36631  regsfromunir1  36722  bj-0eltag  37285  bj-minftyccb  37539  finxpreclem4  37710  fdc  38066  reheibor  38160  0prjspnlem  43056  0prjspnrel  43060  pw2f1ocnv  43465  onexoegt  43672  2omomeqom  43731  omnord1ex  43732  oege2  43735  oenord1ex  43743  oenord1  43744  oaomoencom  43745  oenassex  43746  comptiunov2i  44133  clsk1indlem4  44471  clsk1indlem1  44472  mnuprdlem3  44701  sucidALTVD  45296  sucidALT  45297  sucidVD  45298  wfaxnul  45423  wfaxinf2  45428  nregmodellem  45443  rfcnpre1  45450  eliuniincex  45539  iocopn  45950  icoopn  45955  islptre  46049  cnrefiisplem  46257  icccncfext  46315  fourierdlem103  46637  fourierdlem104  46638  iooborel  46779  sprsymrelfo  47957  sbgoldbo  48263  stgr1  48437  isubgr3stgrlem7  48448  gpg3kgrtriexlem5  48563  pglem  48567  grlimedgnedg  48607  0even  48713  2even  48715  2zrngamgm  48721  zlmodzxzldeplem3  48978  rrx2pxel  49187  rrx2pyel  49188  rrx2linesl  49219  2sphere0  49226  i0oii  49395  io1ii  49396  setc1onsubc  50077