Theorem sseqtri 4019

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 4012	. 2 ⊢ (𝐴 ⊆ 𝐵 ↔ 𝐴 ⊆ 𝐶)
4	1, 3	mpbi 229	1 ⊢ 𝐴 ⊆ 𝐶

Syntax hints:   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  sseqtrri  4020  eqimssi  4043  abssi  4068  ssun2  4174  unixpss  5811  0ima  6078  fvssunirnOLD  6926  mptexgf  7224  difex2  7747  oelim2  8595  omopthlem2  8659  sbthlem7  9089  unifpw  9355  fiuni  9423  dmttrcl  9716  rnttrcl  9717  ttrclexg  9718  rankuni  9858  rankc2  9866  rankxpu  9871  rankmapu  9873  rankxplim  9874  infxpenlem  10008  cf0  10246  fin23lem17  10333  fin23lem31  10338  smobeth  10581  nqerf  10925  dmrecnq  10963  ackbijnn  15774  divalglem2  16338  divalglem5  16340  bitsfzolem  16375  0bits  16380  bezoutlem2  16482  bezoutlem3  16483  lcmcllem  16533  lcmledvds  16536  lcmfval  16558  lcmfcllem  16562  lcmfledvds  16569  odzcllem  16725  odzdvds  16728  unbenlem  16841  4sqlem13  16890  4sqlem14  16891  4sqlem17  16894  4sqlem18  16895  vdwlem8  16921  vdwnnlem3  16930  ramcl2lem  16942  ramtcl  16943  ramtub  16945  strle1  17091  prdsvallem  17400  wunfunc  17849  wunfuncOLD  17850  wunnat  17907  wunnatOLD  17908  psssdm2  18534  tsrss  18542  gicer  19150  symgsssg  19335  symgfisg  19336  odfval  19400  odlem2  19407  gexlem2  19450  torsubg  19722  dprd2da  19912  zringlpirlem2  21033  zringlpirlem3  21034  pjfval  21261  pjpm  21263  toponsspwpw  22424  eltg4i  22463  ntrss2  22561  isopn3  22570  mretopd  22596  leordtval2  22716  ptbasfi  23085  hmphtop  23282  hmpher  23288  restutop  23742  ucnprima  23787  tngtopn  24167  tgioo  24312  xrtgioo  24322  ovolicc2lem4  25037  nulmbl2  25053  iundisj  25065  dyadmax  25115  i1f1  25207  dvfval  25414  dvcnp2  25437  lhop1lem  25530  lhop2  25532  elqaalem1  25832  elqaalem3  25834  taylthlem2  25886  pserulm  25934  psercn2  25935  psercnlem2  25936  psercnlem1  25937  psercn  25938  pserdvlem1  25939  pserdvlem2  25940  pserdv  25941  pserdv2  25942  abelth  25953  dvlog  26159  efopnlem2  26165  logtayl  26168  cxpcn3lem  26255  cxpcn3  26256  resqrtcn  26257  dvatan  26440  atancn  26441  rlimcnp  26470  rlimcnp2  26471  wilthlem3  26574  ftalem4  26580  ftalem5  26581  dchrisum0lem2a  27020  bdayimaon  27196  noetasuplem4  27239  noetainflem4  27243  nocvxminlem  27279  nocvxmin  27280  noeta2  27286  etasslt2  27315  scutbdaybnd2lim  27318  bday1s  27332  lrrecfr  27427  negsunif  27529  cchhllem  28144  cchhllemOLD  28145  axlowdimlem6  28205  hhssabloilem  30514  choc1  30580  chub2i  30723  span0  30795  spanuni  30797  sshhococi  30799  chsup0  30801  spansnpji  30831  mayetes3i  30982  nlelshi  31313  pjimai  31429  pj3i  31461  shatomistici  31614  hatomistici  31615  atcvat4i  31650  iundisjf  31820  rinvf1o  31854  mptctf  31942  iundisjfi  32007  xrge0mulgnn0  32190  gsumpart  32207  fermltlchr  32478  znfermltl  32479  ply1degltel  32666  ply1degltlss  32667  ccfldsrarelvec  32745  ccfldextdgrr  32746  xrge0iifcnv  32913  xrge0iifiso  32915  xrge0iifhom  32917  esumcvgsum  33086  coinfliprv  33481  signsply0  33562  signstcl  33576  signstf  33577  kur14lem6  34202  mthmsta  34569  gg-dvcnp2  35174  gg-psercn2  35178  filnetlem3  35265  filnetlem4  35266  onint1  35334  oninhaus  35335  bj-nuliotaALT  35939  imadifss  36463  poimirlem3  36491  poimirlem32  36520  dvtan  36538  itg2addnclem2  36540  ftc1anclem6  36566  heiborlem3  36681  isdrngo2  36826  elrfi  41432  mapfzcons1  41455  eldioph4b  41549  dnnumch3lem  41788  dnnumch3  41789  dgraalem  41887  dgraaub  41890  resnonrel  42343  cotrcltrcl  42476  cotrclrcl  42493  frege131d  42515  binomcxplemdvbinom  43112  binomcxplemdvsum  43114  binomcxplemnotnn0  43115  relopabVD  43662  rabexgf  43708  fzssnn0  44027  iuneqfzuzlem  44044  allbutfiinf  44130  uzublem  44140  sumnnodd  44346  lptioo2cn  44361  lptioo1cn  44362  fourierdlem31  44854  fourierdlem102  44924  fourierdlem114  44936  fouriercn  44948  elaa2lem  44949  etransclem48  44998  salexct  45050  salgencntex  45059  sge0resplit  45122  meaiuninclem  45196  caratheodorylem1  45242  hoicvr  45264  hoicvrrex  45272  hoidmvlelem3  45313  hoidmvlelem4  45314