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 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 2708

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

This theorem is referenced by:  3eltr4i  2849  vex  3444  opi1  5416  opi2  5417  frrlem14  8241  seqomlem3  8383  nlim2  8417  oneo  8508  nnneo  8583  0elixp  8867  ac6sfi  9184  tz9.13  9703  rankval  9728  rankid  9745  ssrankr1  9747  rankel  9751  rankval3  9752  rankpw  9755  rankss  9761  ranksn  9766  rankuni2  9767  rankun  9768  rankpr  9769  rankop  9770  rankeq0  9773  rankr1b  9776  djuun  9838  dju1dif  10083  isfin4p1  10225  fin1a2lem4  10313  fin1a2lem6  10315  hsmexlem6  10341  dcomex  10357  axdc3lem4  10363  canthp1lem2  10564  pwxpndom2  10576  rankcf  10688  grutsk  10733  axgroth3  10742  inaprc  10747  1lt2pi  10816  pnfxr  11186  mnfxr  11189  1nn  12156  uzrdg0i  13882  axdc4uzlem  13906  ccat2s1p2  14554  wrdl3s3  14885  infcvgaux1i  15780  0bits  16366  sadcf  16380  prmreclem6  16849  fnpr2ob  17479  setcepi  18012  setc2obas  18018  setc2ohom  18019  cat1  18021  smndex1mnd  18835  smndex1id  18836  pwmnd  18862  grpss  18884  psgnunilem2  19424  psgnprfval2  19452  efgi0  19649  efgi1  19650  vrgpf  19697  vrgpinv  19698  frgpuptinv  19700  frgpup2  19705  frgpnabllem1  19802  dmdprdpr  19980  dprdpr  19981  pzriprnglem7  21442  pzriprnglem13  21448  pzriprng1ALT  21451  m2detleiblem3  22573  m2detleiblem4  22574  m2detleib  22575  leordtval2  23156  xpstopnlem1  23753  xpstopnlem2  23755  ptcmp  24002  tsmsfbas  24072  zcld  24758  sszcld  24762  abscncfALT  24874  iimulcn  24890  iimulcnOLD  24891  icopnfhmeo  24897  iccpnfhmeo  24899  xrhmeo  24900  cnstrcvs  25097  cncvs  25101  dveflem  25939  ftc1  26005  efopnlem2  26622  cxpcn3  26714  efrlim  26935  efrlimOLD  26936  precsexlem11  28213  1nns  28345  structvtxval  29094  usgrexmplef  29332  wwlks2onv  30026  elwwlks2ons3im  30027  usgrwwlks2on  30031  umgrwwlks2on  30032  konigsberglem4  30330  hhshsslem2  31343  nonbooli  31726  nmopadjlei  32163  cshw1s2  33042  fzto1st  33185  cyc2fv1  33203  cyc3fv1  33219  cyc3fv2  33220  cyc3evpm  33232  1arithidom  33618  zringpid  33633  vieta  33736  xrge0iifhmeo  34093  dya2iocbrsiga  34432  dya2icobrsiga  34433  fib0  34556  fib1  34557  coinflippvt  34642  prodfzo03  34760  circlevma  34799  circlemethhgt  34800  hgt750lemg  34811  hgt750lemb  34813  hgt750lema  34814  hgt750leme  34815  tgoldbachgtde  34817  tgoldbachgt  34820  bnj97  35022  bnj553  35054  bnj966  35100  bnj1442  35205  fineqvnttrclse  35280  fineqvinfep  35281  subfacp1lem2a  35374  subfacp1lem5  35378  erdszelem5  35389  erdszelem8  35392  ex-sategoelel12  35621  rankeq1o  36365  0hf  36371  onint1  36643  regsfromunir1  36670  bj-0eltag  37179  bj-minftyccb  37430  finxpreclem4  37599  fdc  37946  reheibor  38040  0prjspnlem  42876  0prjspnrel  42880  pw2f1ocnv  43289  onexoegt  43496  2omomeqom  43555  omnord1ex  43556  oege2  43559  oenord1ex  43567  oenord1  43568  oaomoencom  43569  oenassex  43570  comptiunov2i  43957  clsk1indlem4  44295  clsk1indlem1  44296  mnuprdlem3  44525  sucidALTVD  45120  sucidALT  45121  sucidVD  45122  wfaxnul  45247  wfaxinf2  45252  nregmodellem  45267  rfcnpre1  45274  eliuniincex  45363  iocopn  45776  icoopn  45781  islptre  45875  cnrefiisplem  46083  icccncfext  46141  fourierdlem103  46463  fourierdlem104  46464  iooborel  46605  sprsymrelfo  47753  sbgoldbo  48043  stgr1  48217  isubgr3stgrlem7  48228  gpg3kgrtriexlem5  48343  pglem  48347  grlimedgnedg  48387  0even  48493  2even  48495  2zrngamgm  48501  zlmodzxzldeplem3  48758  rrx2pxel  48967  rrx2pyel  48968  rrx2linesl  48999  2sphere0  49006  i0oii  49175  io1ii  49176  setc1onsubc  49857