Theorem eleqtrri 2830

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

Syntax hints:   = wceq 1539   ∈ wcel 2104

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1780  df-cleq 2722  df-clel 2808

This theorem is referenced by:  3eltr4i  2844  vex  3476  vexOLD  3477  opi1  5467  opi2  5468  frrlem14  8286  wfrlem14OLD  8324  wfrlem16OLD  8326  seqomlem3  8454  nlim2  8492  oneo  8583  nnneo  8656  0elixp  8925  ac6sfi  9289  tz9.13  9788  rankval  9813  rankid  9830  ssrankr1  9832  rankel  9836  rankval3  9837  rankpw  9840  rankss  9846  ranksn  9851  rankuni2  9852  rankun  9853  rankpr  9854  rankop  9855  rankeq0  9858  rankr1b  9861  djuun  9923  dju1dif  10169  isfin4p1  10312  fin1a2lem4  10400  fin1a2lem6  10402  hsmexlem6  10428  dcomex  10444  axdc3lem4  10450  canthp1lem2  10650  pwxpndom2  10662  rankcf  10774  grutsk  10819  axgroth3  10828  inaprc  10833  1lt2pi  10902  pnfxr  11272  mnfxr  11275  1nn  12227  uzrdg0i  13928  axdc4uzlem  13952  ccat2s1p2  14584  wrdl3s3  14917  infcvgaux1i  15807  0bits  16384  sadcf  16398  prmreclem6  16858  fnpr2ob  17508  setcepi  18042  setc2obas  18048  setc2ohom  18049  cat1  18051  smndex1mnd  18827  smndex1id  18828  pwmnd  18854  grpss  18876  psgnunilem2  19404  psgnprfval2  19432  efgi0  19629  efgi1  19630  vrgpf  19677  vrgpinv  19678  frgpuptinv  19680  frgpup2  19685  frgpnabllem1  19782  dmdprdpr  19960  dprdpr  19961  pzriprnglem7  21256  pzriprnglem13  21262  pzriprng1ALT  21265  m2detleiblem3  22351  m2detleiblem4  22352  m2detleib  22353  leordtval2  22936  xpstopnlem1  23533  xpstopnlem2  23535  ptcmp  23782  tsmsfbas  23852  zcld  24549  sszcld  24553  abscncfALT  24665  iimulcn  24681  iimulcnOLD  24682  icopnfhmeo  24688  iccpnfhmeo  24690  xrhmeo  24691  cnstrcvs  24888  cncvs  24892  dveflem  25731  ftc1  25794  efopnlem2  26401  cxpcn3  26492  efrlim  26710  precsexlem11  27902  0n0s  27939  structvtxval  28548  usgrexmplef  28783  wwlks2onv  29474  elwwlks2ons3im  29475  umgrwwlks2on  29478  konigsberglem4  29775  hhshsslem2  30788  nonbooli  31171  nmopadjlei  31608  cshw1s2  32391  fzto1st  32532  cyc2fv1  32550  cyc3fv1  32566  cyc3fv2  32567  cyc3evpm  32579  xrge0iifhmeo  33214  dya2iocbrsiga  33572  dya2icobrsiga  33573  fib0  33696  fib1  33697  coinflippvt  33781  prodfzo03  33913  circlevma  33952  circlemethhgt  33953  hgt750lemg  33964  hgt750lemb  33966  hgt750lema  33967  hgt750leme  33968  tgoldbachgtde  33970  tgoldbachgt  33973  bnj97  34175  bnj553  34207  bnj966  34253  bnj1442  34358  subfacp1lem2a  34469  subfacp1lem5  34473  erdszelem5  34484  erdszelem8  34487  ex-sategoelel12  34716  rankeq1o  35447  0hf  35453  onint1  35637  bj-0eltag  36162  bj-minftyccb  36409  finxpreclem4  36578  fdc  36916  reheibor  37010  0prjspnlem  41667  0prjspnrel  41671  pw2f1ocnv  42078  onexoegt  42295  2omomeqom  42355  omnord1ex  42356  oege2  42359  oenord1ex  42367  oenord1  42368  oaomoencom  42369  oenassex  42370  comptiunov2i  42759  clsk1indlem4  43097  clsk1indlem1  43098  mnuprdlem3  43335  sucidALTVD  43933  sucidALT  43934  sucidVD  43935  rfcnpre1  44005  eliuniincex  44099  iocopn  44531  icoopn  44536  islptre  44633  cnrefiisplem  44843  icccncfext  44901  fourierdlem103  45223  fourierdlem104  45224  iooborel  45365  upwordnul  45892  upwordsing  45896  sprsymrelfo  46463  sbgoldbo  46753  0even  46917  2even  46919  2zrngamgm  46925  zlmodzxzldeplem3  47270  rrx2pxel  47484  rrx2pyel  47485  rrx2linesl  47516  2sphere0  47523  i0oii  47639  io1ii  47640