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

Syntax hints:   = wceq 1541   ∈ wcel 2111

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 2113  ax-9 2121  ax-ext 2703

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

This theorem is referenced by:  3eltr4i  2844  vex  3440  opi1  5406  opi2  5407  frrlem14  8229  seqomlem3  8371  nlim2  8405  oneo  8496  nnneo  8570  0elixp  8853  ac6sfi  9168  tz9.13  9684  rankval  9709  rankid  9726  ssrankr1  9728  rankel  9732  rankval3  9733  rankpw  9736  rankss  9742  ranksn  9747  rankuni2  9748  rankun  9749  rankpr  9750  rankop  9751  rankeq0  9754  rankr1b  9757  djuun  9819  dju1dif  10064  isfin4p1  10206  fin1a2lem4  10294  fin1a2lem6  10296  hsmexlem6  10322  dcomex  10338  axdc3lem4  10344  canthp1lem2  10544  pwxpndom2  10556  rankcf  10668  grutsk  10713  axgroth3  10722  inaprc  10727  1lt2pi  10796  pnfxr  11166  mnfxr  11169  1nn  12136  uzrdg0i  13866  axdc4uzlem  13890  ccat2s1p2  14538  wrdl3s3  14869  infcvgaux1i  15764  0bits  16350  sadcf  16364  prmreclem6  16833  fnpr2ob  17462  setcepi  17995  setc2obas  18001  setc2ohom  18002  cat1  18004  smndex1mnd  18818  smndex1id  18819  pwmnd  18845  grpss  18867  psgnunilem2  19407  psgnprfval2  19435  efgi0  19632  efgi1  19633  vrgpf  19680  vrgpinv  19681  frgpuptinv  19683  frgpup2  19688  frgpnabllem1  19785  dmdprdpr  19963  dprdpr  19964  pzriprnglem7  21424  pzriprnglem13  21430  pzriprng1ALT  21433  m2detleiblem3  22544  m2detleiblem4  22545  m2detleib  22546  leordtval2  23127  xpstopnlem1  23724  xpstopnlem2  23726  ptcmp  23973  tsmsfbas  24043  zcld  24729  sszcld  24733  abscncfALT  24845  iimulcn  24861  iimulcnOLD  24862  icopnfhmeo  24868  iccpnfhmeo  24870  xrhmeo  24871  cnstrcvs  25068  cncvs  25072  dveflem  25910  ftc1  25976  efopnlem2  26593  cxpcn3  26685  efrlim  26906  efrlimOLD  26907  precsexlem11  28155  1nns  28277  structvtxval  28999  usgrexmplef  29237  wwlks2onv  29931  elwwlks2ons3im  29932  usgrwwlks2on  29936  umgrwwlks2on  29937  konigsberglem4  30235  hhshsslem2  31248  nonbooli  31631  nmopadjlei  32068  cshw1s2  32941  fzto1st  33072  cyc2fv1  33090  cyc3fv1  33106  cyc3fv2  33107  cyc3evpm  33119  1arithidom  33502  zringpid  33517  xrge0iifhmeo  33949  dya2iocbrsiga  34288  dya2icobrsiga  34289  fib0  34412  fib1  34413  coinflippvt  34498  prodfzo03  34616  circlevma  34655  circlemethhgt  34656  hgt750lemg  34667  hgt750lemb  34669  hgt750lema  34670  hgt750leme  34671  tgoldbachgtde  34673  tgoldbachgt  34676  bnj97  34878  bnj553  34910  bnj966  34956  bnj1442  35061  fineqvnttrclse  35144  subfacp1lem2a  35224  subfacp1lem5  35228  erdszelem5  35239  erdszelem8  35242  ex-sategoelel12  35471  rankeq1o  36215  0hf  36221  onint1  36493  bj-0eltag  37022  bj-minftyccb  37269  finxpreclem4  37438  fdc  37795  reheibor  37889  0prjspnlem  42726  0prjspnrel  42730  pw2f1ocnv  43140  onexoegt  43347  2omomeqom  43406  omnord1ex  43407  oege2  43410  oenord1ex  43418  oenord1  43419  oaomoencom  43420  oenassex  43421  comptiunov2i  43809  clsk1indlem4  44147  clsk1indlem1  44148  mnuprdlem3  44377  sucidALTVD  44972  sucidALT  44973  sucidVD  44974  wfaxnul  45099  wfaxinf2  45104  nregmodellem  45119  rfcnpre1  45126  eliuniincex  45216  iocopn  45630  icoopn  45635  islptre  45729  cnrefiisplem  45937  icccncfext  45995  fourierdlem103  46317  fourierdlem104  46318  iooborel  46459  sprsymrelfo  47607  sbgoldbo  47897  stgr1  48071  isubgr3stgrlem7  48082  gpg3kgrtriexlem5  48197  pglem  48201  grlimedgnedg  48241  0even  48347  2even  48349  2zrngamgm  48355  zlmodzxzldeplem3  48613  rrx2pxel  48822  rrx2pyel  48823  rrx2linesl  48854  2sphere0  48861  i0oii  49030  io1ii  49031  setc1onsubc  49713