Theorem sseqtri 3961

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

Syntax hints:   = wceq 1541   ⊆ wss 3891

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1801  ax-4 1815  ax-5 1916  ax-6 1974  ax-7 2014  ax-8 2111  ax-9 2119  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1544  df-ex 1786  df-sb 2071  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3432  df-in 3898  df-ss 3908

This theorem is referenced by:  sseqtrri  3962  eqimssi  3983  abssi  4007  ssun2  4111  unixpss  5717  0ima  5983  fvssunirn  6797  mptexgf  7092  difex2  7601  oelim2  8402  omopthlem2  8464  sbthlem7  8845  unifpw  9083  fiuni  9148  dmttrcl  9440  rnttrcl  9441  ttrclexg  9442  rankuni  9605  rankc2  9613  rankxpu  9618  rankmapu  9620  rankxplim  9621  infxpenlem  9753  cf0  9991  fin23lem17  10078  fin23lem31  10083  smobeth  10326  nqerf  10670  dmrecnq  10708  ackbijnn  15521  divalglem2  16085  divalglem5  16087  bitsfzolem  16122  0bits  16127  bezoutlem2  16229  bezoutlem3  16230  lcmcllem  16282  lcmledvds  16285  lcmfval  16307  lcmfcllem  16311  lcmfledvds  16318  odzcllem  16474  odzdvds  16477  unbenlem  16590  4sqlem13  16639  4sqlem14  16640  4sqlem17  16643  4sqlem18  16644  vdwlem8  16670  vdwnnlem3  16679  ramcl2lem  16691  ramtcl  16692  ramtub  16694  strle1  16840  prdsvallem  17146  wunfunc  17595  wunfuncOLD  17596  wunnat  17653  wunnatOLD  17654  psssdm2  18280  tsrss  18288  gicer  18873  symgsssg  19056  symgfisg  19057  odfval  19121  odlem2  19128  gexlem2  19168  torsubg  19436  dprd2da  19626  zringlpirlem2  20666  zringlpirlem3  20667  pjfval  20894  pjpm  20896  toponsspwpw  22052  eltg4i  22091  ntrss2  22189  isopn3  22198  mretopd  22224  leordtval2  22344  ptbasfi  22713  hmphtop  22910  hmpher  22916  restutop  23370  ucnprima  23415  tngtopn  23795  tgioo  23940  xrtgioo  23950  ovolicc2lem4  24665  nulmbl2  24681  iundisj  24693  dyadmax  24743  i1f1  24835  dvfval  25042  dvcnp2  25065  lhop1lem  25158  lhop2  25160  elqaalem1  25460  elqaalem3  25462  taylthlem2  25514  pserulm  25562  psercn2  25563  psercnlem2  25564  psercnlem1  25565  psercn  25566  pserdvlem1  25567  pserdvlem2  25568  pserdv  25569  pserdv2  25570  abelth  25581  dvlog  25787  efopnlem2  25793  logtayl  25796  cxpcn3lem  25881  cxpcn3  25882  resqrtcn  25883  dvatan  26066  atancn  26067  rlimcnp  26096  rlimcnp2  26097  wilthlem3  26200  ftalem4  26206  ftalem5  26207  dchrisum0lem2a  26646  cchhllem  27235  cchhllemOLD  27236  axlowdimlem6  27296  hhssabloilem  29602  choc1  29668  chub2i  29811  span0  29883  spanuni  29885  sshhococi  29887  chsup0  29889  spansnpji  29919  mayetes3i  30070  nlelshi  30401  pjimai  30517  pj3i  30549  shatomistici  30702  hatomistici  30703  atcvat4i  30738  iundisjf  30907  rinvf1o  30944  mptctf  31031  iundisjfi  31096  xrge0mulgnn0  31277  gsumpart  31294  znfermltl  31541  ccfldsrarelvec  31720  ccfldextdgrr  31721  xrge0iifcnv  31862  xrge0iifiso  31864  xrge0iifhom  31866  esumcvgsum  32035  coinfliprv  32428  signsply0  32509  signstcl  32523  signstf  32524  kur14lem6  33152  mthmsta  33519  bdayimaon  33875  noetasuplem4  33918  noetainflem4  33922  nocvxminlem  33951  nocvxmin  33952  noeta2  33958  etasslt2  33987  scutbdaybnd2lim  33990  bday1s  34004  lrrecfr  34079  filnetlem3  34548  filnetlem4  34549  onint1  34617  oninhaus  34618  bj-nuliotaALT  35208  imadifss  35731  poimirlem3  35759  poimirlem32  35788  dvtan  35806  itg2addnclem2  35808  ftc1anclem6  35834  heiborlem3  35950  isdrngo2  36095  elrfi  40496  mapfzcons1  40519  eldioph4b  40613  dnnumch3lem  40851  dnnumch3  40852  dgraalem  40950  dgraaub  40953  resnonrel  41153  cotrcltrcl  41286  cotrclrcl  41303  frege131d  41325  binomcxplemdvbinom  41924  binomcxplemdvsum  41926  binomcxplemnotnn0  41927  relopabVD  42474  rabexgf  42520  fzssnn0  42810  iuneqfzuzlem  42827  allbutfiinf  42914  uzublem  42924  sumnnodd  43125  lptioo2cn  43140  lptioo1cn  43141  fourierdlem31  43633  fourierdlem102  43703  fourierdlem114  43715  fouriercn  43727  elaa2lem  43728  etransclem48  43777  salexct  43827  salgencntex  43836  sge0resplit  43898  meaiuninclem  43972  caratheodorylem1  44018  hoicvr  44040  hoicvrrex  44048  hoidmvlelem3  44089  hoidmvlelem4  44090