Theorem sseqtri 3984

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

Syntax hints:   = wceq 1540   ⊆ wss 3903

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3920

This theorem is referenced by:  sseqtrri  3985  3sstr3i  3986  eqimssi  3996  abssi  4021  ssun2  4130  unixpss  5753  0ima  6029  fvssunirnOLD  6854  mptexgf  7158  difex2  7696  oelim2  8513  omopthlem2  8578  sbthlem7  9010  unifpw  9245  fiuni  9318  dmttrcl  9617  rnttrcl  9618  ttrclexg  9619  rankuni  9759  rankc2  9767  rankxpu  9772  rankmapu  9774  rankxplim  9775  infxpenlem  9907  cf0  10145  fin23lem17  10232  fin23lem31  10237  smobeth  10480  nqerf  10824  dmrecnq  10862  ackbijnn  15735  divalglem2  16306  divalglem5  16308  bitsfzolem  16345  0bits  16350  bezoutlem2  16451  bezoutlem3  16452  lcmcllem  16507  lcmledvds  16510  lcmfval  16532  lcmfcllem  16536  lcmfledvds  16543  odzcllem  16704  odzdvds  16707  unbenlem  16820  4sqlem13  16869  4sqlem14  16870  4sqlem17  16873  4sqlem18  16874  vdwlem8  16900  vdwnnlem3  16909  ramcl2lem  16921  ramtcl  16922  ramtub  16924  strle1  17069  prdsvallem  17358  wunfunc  17808  wunnat  17866  psssdm2  18487  tsrss  18495  gicer  19156  symgsssg  19346  symgfisg  19347  odfval  19411  odlem2  19418  gexlem2  19461  torsubg  19733  dprd2da  19923  zringlpirlem2  21370  zringlpirlem3  21371  fermltlchr  21436  pjfval  21613  pjpm  21615  toponsspwpw  22807  eltg4i  22845  ntrss2  22942  isopn3  22951  mretopd  22977  leordtval2  23097  ptbasfi  23466  hmphtop  23663  hmpher  23669  restutop  24123  ucnprima  24167  tngtopn  24536  tgioo  24682  xrtgioo  24693  ovolicc2lem4  25419  nulmbl2  25435  iundisj  25447  dyadmax  25497  i1f1  25589  dvfval  25796  dvcnp2  25819  dvcnp2OLD  25820  lhop1lem  25916  lhop2  25918  elqaalem1  26225  elqaalem3  26227  taylthlem2  26280  taylthlem2OLD  26281  pserulm  26329  psercn2  26330  psercn2OLD  26331  psercnlem2  26332  psercnlem1  26333  psercn  26334  pserdvlem1  26335  pserdvlem2  26336  pserdv  26337  pserdv2  26338  abelth  26349  dvlog  26558  efopnlem2  26564  logtayl  26567  cxpcn3lem  26655  cxpcn3  26656  resqrtcn  26657  dvatan  26843  atancn  26844  rlimcnp  26873  rlimcnp2  26874  wilthlem3  26978  ftalem4  26984  ftalem5  26985  dchrisum0lem2a  27426  bdayimaon  27603  noetasuplem4  27646  noetainflem4  27650  nobdaymin  27687  nocvxminlem  27688  noeta2  27695  etasslt2  27725  scutbdaybnd2lim  27728  bday1s  27745  lrrecfr  27855  addsbdaylem  27928  negsunif  27966  onsiso  28174  bdayon  28178  zs12bday  28361  cchhllem  28832  axlowdimlem6  28892  hhssabloilem  31205  choc1  31271  chub2i  31414  span0  31486  spanuni  31488  sshhococi  31490  chsup0  31492  spansnpji  31522  mayetes3i  31673  nlelshi  32004  pjimai  32120  pj3i  32152  shatomistici  32305  hatomistici  32306  atcvat4i  32341  iundisjf  32533  rinvf1o  32573  mptctf  32660  iundisjfi  32739  xrge0mulgnn0  32969  gsumpart  33010  znfermltl  33303  ply1degltel  33527  ply1degleel  33528  ply1degltlss  33529  ccfldsrarelvec  33638  ccfldextdgrr  33639  2sqr3minply  33747  xrge0iifcnv  33900  xrge0iifiso  33902  xrge0iifhom  33904  esumcvgsum  34055  coinfliprv  34451  signsply0  34519  signstcl  34533  signstf  34534  kur14lem6  35184  mthmsta  35551  filnetlem3  36354  filnetlem4  36355  onint1  36423  oninhaus  36424  bj-nuliotaALT  37032  imadifss  37575  poimirlem3  37603  poimirlem32  37632  dvtan  37650  itg2addnclem2  37652  ftc1anclem6  37678  heiborlem3  37793  isdrngo2  37938  elrfi  42667  mapfzcons1  42690  eldioph4b  42784  dnnumch3lem  43019  dnnumch3  43020  dgraalem  43118  dgraaub  43121  resnonrel  43565  cotrcltrcl  43698  cotrclrcl  43715  frege131d  43737  binomcxplemdvbinom  44326  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  relopabVD  44874  rabexgf  45002  fzssnn0  45298  iuneqfzuzlem  45314  allbutfiinf  45399  uzublem  45409  sumnnodd  45611  lptioo2cn  45626  lptioo1cn  45627  fourierdlem31  46119  fourierdlem102  46189  fourierdlem114  46201  fouriercn  46213  elaa2lem  46214  etransclem48  46263  salexct  46315  salgencntex  46324  sge0resplit  46387  meaiuninclem  46461  caratheodorylem1  46507  hoicvr  46529  hoicvrrex  46537  hoidmvlelem3  46578  hoidmvlelem4  46579  gricrel  47903  grlicrel  47990