Theorem sseqtri 4005

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

Syntax hints:   = wceq 1537   ⊆ wss 3938

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 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2802  df-cleq 2816  df-clel 2895  df-in 3945  df-ss 3954

This theorem is referenced by:  sseqtrri  4006  eqimssi  4027  abssi  4048  ssun2  4151  unixpss  5685  0ima  5948  fvssunirn  6701  mptexgf  6987  difex2  7484  oelim2  8223  omopthlem2  8285  sbthlem7  8635  unifpw  8829  fiuni  8894  rankuni  9294  rankc2  9302  rankxpu  9307  rankmapu  9309  rankxplim  9310  infxpenlem  9441  cf0  9675  fin23lem17  9762  fin23lem31  9767  smobeth  10010  nqerf  10354  dmrecnq  10392  ackbijnn  15185  divalglem2  15748  divalglem5  15750  bitsfzolem  15785  0bits  15790  bezoutlem2  15890  bezoutlem3  15891  lcmcllem  15942  lcmledvds  15945  lcmfval  15967  lcmfcllem  15971  lcmfledvds  15978  odzcllem  16131  odzdvds  16134  unbenlem  16246  4sqlem13  16295  4sqlem14  16296  4sqlem17  16299  4sqlem18  16300  vdwlem8  16326  vdwnnlem3  16335  ramcl2lem  16347  ramtcl  16348  ramtub  16350  strle1  16594  prdsval  16730  wunfunc  17171  wunnat  17228  psssdm2  17827  tsrss  17835  gicer  18418  symgsssg  18597  symgfisg  18598  odfval  18662  odlem2  18669  gexlem2  18709  torsubg  18976  dprd2da  19166  zringlpirlem2  20634  zringlpirlem3  20635  pjfval  20852  pjpm  20854  toponsspwpw  21532  eltg4i  21570  ntrss2  21667  isopn3  21676  mretopd  21702  leordtval2  21822  ptbasfi  22191  hmphtop  22388  hmpher  22394  restutop  22848  ucnprima  22893  tngtopn  23261  tgioo  23406  xrtgioo  23416  ovolicc2lem4  24123  nulmbl2  24139  iundisj  24151  dyadmax  24201  i1f1  24293  dvfval  24497  dvcnp2  24519  lhop1lem  24612  lhop2  24614  elqaalem1  24910  elqaalem3  24912  taylthlem2  24964  pserulm  25012  psercn2  25013  psercnlem2  25014  psercnlem1  25015  psercn  25016  pserdvlem1  25017  pserdvlem2  25018  pserdv  25019  pserdv2  25020  abelth  25031  dvlog  25236  efopnlem2  25242  logtayl  25245  cxpcn3lem  25330  cxpcn3  25331  resqrtcn  25332  dvatan  25515  atancn  25516  rlimcnp  25545  rlimcnp2  25546  wilthlem3  25649  ftalem4  25655  ftalem5  25656  dchrisum0lem2a  26095  cchhllem  26675  axlowdimlem6  26735  hhssabloilem  29040  choc1  29106  chub2i  29249  span0  29321  spanuni  29323  sshhococi  29325  chsup0  29327  spansnpji  29357  mayetes3i  29508  nlelshi  29839  pjimai  29955  pj3i  29987  shatomistici  30140  hatomistici  30141  atcvat4i  30176  iundisjf  30341  rinvf1o  30377  mptctf  30455  iundisjfi  30521  xrge0mulgnn0  30678  ccfldsrarelvec  31058  ccfldextdgrr  31059  xrge0iifcnv  31178  xrge0iifiso  31180  xrge0iifhom  31182  esumcvgsum  31349  coinfliprv  31742  signsply0  31823  signstcl  31837  signstf  31838  kur14lem6  32460  mthmsta  32827  bdayimaon  33199  nosupbday  33207  noetalem3  33221  noetalem4  33222  nocvxminlem  33249  nocvxmin  33250  filnetlem3  33730  filnetlem4  33731  onint1  33799  oninhaus  33800  bj-nuliotaALT  34353  imadifss  34869  poimirlem3  34897  poimirlem32  34926  dvtan  34944  itg2addnclem2  34946  ftc1anclem6  34974  heiborlem3  35093  isdrngo2  35238  elrfi  39298  mapfzcons1  39321  eldioph4b  39415  dnnumch3lem  39653  dnnumch3  39654  dgraalem  39752  dgraaub  39755  resnonrel  39959  cotrcltrcl  40077  cotrclrcl  40094  frege131d  40116  binomcxplemdvbinom  40692  binomcxplemdvsum  40694  binomcxplemnotnn0  40695  relopabVD  41242  rabexgf  41288  fzssnn0  41592  iuneqfzuzlem  41609  allbutfiinf  41701  uzublem  41711  sumnnodd  41918  lptioo2cn  41933  lptioo1cn  41934  fourierdlem31  42430  fourierdlem102  42500  fourierdlem114  42512  fouriercn  42524  elaa2lem  42525  etransclem48  42574  salexct  42624  salgencntex  42633  sge0resplit  42695  meaiuninclem  42769  caratheodorylem1  42815  hoicvr  42837  hoicvrrex  42845  hoidmvlelem3  42886  hoidmvlelem4  42887