Theorem sseqtri 3970

Description: Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)

Hypotheses

Ref	Expression
sseqtr.1	⊢ 𝐴 ⊆ 𝐵
sseqtr.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
sseqtri	⊢ 𝐴 ⊆ 𝐶

Proof of Theorem sseqtri

Step	Hyp	Ref	Expression
1		sseqtr.1	. 2 ⊢ 𝐴 ⊆ 𝐵
2		sseqtr.2	. . 3 ⊢ 𝐵 = 𝐶
3	2	sseq2i 3951	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶)
4	1, 3	mpbi 230	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1542   ⊆ wss 3889

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-9 2124  ax-ext 2708

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

This theorem is referenced by:  sseqtrri  3971  3sstr3i  3972  eqimssi  3982  abssi  4008  ssun2  4119  unixpss  5766  0ima  6043  mptexgf  7177  difex2  7714  oelim2  8531  omopthlem2  8596  sbthlem7  9031  unifpw  9265  fiuni  9341  dmttrcl  9642  rnttrcl  9643  ttrclexg  9644  rankuni  9787  rankc2  9795  rankxpu  9800  rankmapu  9802  rankxplim  9803  infxpenlem  9935  cf0  10173  fin23lem17  10260  fin23lem31  10265  smobeth  10509  nqerf  10853  dmrecnq  10891  ackbijnn  15793  divalglem2  16364  divalglem5  16366  bitsfzolem  16403  0bits  16408  bezoutlem2  16509  bezoutlem3  16510  lcmcllem  16565  lcmledvds  16568  lcmfval  16590  lcmfcllem  16594  lcmfledvds  16601  odzcllem  16763  odzdvds  16766  unbenlem  16879  4sqlem13  16928  4sqlem14  16929  4sqlem17  16932  4sqlem18  16933  vdwlem8  16959  vdwnnlem3  16968  ramcl2lem  16980  ramtcl  16981  ramtub  16983  strle1  17128  prdsvallem  17417  wunfunc  17868  wunnat  17926  psssdm2  18547  tsrss  18555  gicer  19252  symgsssg  19442  symgfisg  19443  odfval  19507  odlem2  19514  gexlem2  19557  torsubg  19829  dprd2da  20019  zringlpirlem2  21443  zringlpirlem3  21444  fermltlchr  21509  pjfval  21686  pjpm  21688  toponsspwpw  22887  eltg4i  22925  ntrss2  23022  isopn3  23031  mretopd  23057  leordtval2  23177  ptbasfi  23546  hmphtop  23743  hmpher  23749  restutop  24202  ucnprima  24246  tngtopn  24615  tgioo  24761  xrtgioo  24772  ovolicc2lem4  25487  nulmbl2  25503  iundisj  25515  dyadmax  25565  i1f1  25657  dvfval  25864  dvcnp2  25887  lhop1lem  25980  lhop2  25982  elqaalem1  26285  elqaalem3  26287  taylthlem2  26339  pserulm  26387  psercn2  26388  psercnlem2  26389  psercnlem1  26390  psercn  26391  pserdvlem1  26392  pserdvlem2  26393  pserdv  26394  pserdv2  26395  abelth  26406  dvlog  26615  efopnlem2  26621  logtayl  26624  cxpcn3lem  26711  cxpcn3  26712  resqrtcn  26713  dvatan  26899  atancn  26900  rlimcnp  26929  rlimcnp2  26930  wilthlem3  27033  ftalem4  27039  ftalem5  27040  dchrisum0lem2a  27480  bdayimaon  27657  noetasuplem4  27700  noetainflem4  27704  nobdaymin  27745  nocvxminlem  27746  noeta2  27753  etaslts2  27786  cutbdaybnd2lim  27789  bday1  27806  lrrecfr  27935  addbdaylem  28009  negsunif  28047  oniso  28263  bdayons  28268  cchhllem  28955  axlowdimlem6  29016  hhssabloilem  31332  choc1  31398  chub2i  31541  span0  31613  spanuni  31615  sshhococi  31617  chsup0  31619  spansnpji  31649  mayetes3i  31800  nlelshi  32131  pjimai  32247  pj3i  32279  shatomistici  32432  hatomistici  32433  atcvat4i  32468  iundisjf  32659  rinvf1o  32703  mptctf  32789  iundisjfi  32869  xrge0mulgnn0  33075  gsumpart  33124  znfermltl  33426  ply1degltel  33654  ply1degleel  33655  ply1degltlss  33656  ccfldsrarelvec  33815  ccfldextdgrr  33816  2sqr3minply  33924  xrge0iifcnv  34077  xrge0iifiso  34079  xrge0iifhom  34081  esumcvgsum  34232  coinfliprv  34627  signsply0  34695  signstcl  34709  signstf  34710  kur14lem6  35393  mthmsta  35760  filnetlem3  36562  filnetlem4  36563  onint1  36631  oninhaus  36632  bj-nuliotaALT  37365  imadifss  37916  poimirlem3  37944  poimirlem32  37973  dvtan  37991  itg2addnclem2  37993  ftc1anclem6  38019  heiborlem3  38134  isdrngo2  38279  elrfi  43126  mapfzcons1  43149  eldioph4b  43239  dnnumch3lem  43474  dnnumch3  43475  dgraalem  43573  dgraaub  43576  resnonrel  44019  cotrcltrcl  44152  cotrclrcl  44169  frege131d  44191  binomcxplemdvbinom  44780  binomcxplemdvsum  44782  binomcxplemnotnn0  44783  relopabVD  45327  rabexgf  45455  fzssnn0  45749  iuneqfzuzlem  45764  allbutfiinf  45848  uzublem  45858  sumnnodd  46060  lptioo2cn  46073  lptioo1cn  46074  fourierdlem31  46566  fourierdlem102  46636  fourierdlem114  46648  fouriercn  46660  elaa2lem  46661  etransclem48  46710  salexct  46762  salgencntex  46771  sge0resplit  46834  meaiuninclem  46908  caratheodorylem1  46954  hoicvr  46976  hoicvrrex  46984  hoidmvlelem3  47025  hoidmvlelem4  47026  gricrel  48395  grlicrel  48482