Theorem sseqtri 4017

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

Syntax hints:   = wceq 1539   ⊆ wss 3947

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  sseqtrri  4018  eqimssi  4041  abssi  4066  ssun2  4172  unixpss  5809  0ima  6076  fvssunirnOLD  6924  mptexgf  7225  difex2  7749  oelim2  8597  omopthlem2  8661  sbthlem7  9091  unifpw  9357  fiuni  9425  dmttrcl  9718  rnttrcl  9719  ttrclexg  9720  rankuni  9860  rankc2  9868  rankxpu  9873  rankmapu  9875  rankxplim  9876  infxpenlem  10010  cf0  10248  fin23lem17  10335  fin23lem31  10340  smobeth  10583  nqerf  10927  dmrecnq  10965  ackbijnn  15778  divalglem2  16342  divalglem5  16344  bitsfzolem  16379  0bits  16384  bezoutlem2  16486  bezoutlem3  16487  lcmcllem  16537  lcmledvds  16540  lcmfval  16562  lcmfcllem  16566  lcmfledvds  16573  odzcllem  16729  odzdvds  16732  unbenlem  16845  4sqlem13  16894  4sqlem14  16895  4sqlem17  16898  4sqlem18  16899  vdwlem8  16925  vdwnnlem3  16934  ramcl2lem  16946  ramtcl  16947  ramtub  16949  strle1  17095  prdsvallem  17404  wunfunc  17853  wunfuncOLD  17854  wunnat  17911  wunnatOLD  17912  psssdm2  18538  tsrss  18546  gicer  19191  symgsssg  19376  symgfisg  19377  odfval  19441  odlem2  19448  gexlem2  19491  torsubg  19763  dprd2da  19953  zringlpirlem2  21234  zringlpirlem3  21235  pjfval  21480  pjpm  21482  toponsspwpw  22644  eltg4i  22683  ntrss2  22781  isopn3  22790  mretopd  22816  leordtval2  22936  ptbasfi  23305  hmphtop  23502  hmpher  23508  restutop  23962  ucnprima  24007  tngtopn  24387  tgioo  24532  xrtgioo  24542  ovolicc2lem4  25269  nulmbl2  25285  iundisj  25297  dyadmax  25347  i1f1  25439  dvfval  25646  dvcnp2  25669  dvcnp2OLD  25670  lhop1lem  25765  lhop2  25767  elqaalem1  26068  elqaalem3  26070  taylthlem2  26122  pserulm  26170  psercn2  26171  psercnlem2  26172  psercnlem1  26173  psercn  26174  pserdvlem1  26175  pserdvlem2  26176  pserdv  26177  pserdv2  26178  abelth  26189  dvlog  26395  efopnlem2  26401  logtayl  26404  cxpcn3lem  26491  cxpcn3  26492  resqrtcn  26493  dvatan  26676  atancn  26677  rlimcnp  26706  rlimcnp2  26707  wilthlem3  26810  ftalem4  26816  ftalem5  26817  dchrisum0lem2a  27256  bdayimaon  27432  noetasuplem4  27475  noetainflem4  27479  nocvxminlem  27515  nocvxmin  27516  noeta2  27522  etasslt2  27552  scutbdaybnd2lim  27555  bday1s  27569  lrrecfr  27665  negsunif  27768  cchhllem  28411  cchhllemOLD  28412  axlowdimlem6  28472  hhssabloilem  30781  choc1  30847  chub2i  30990  span0  31062  spanuni  31064  sshhococi  31066  chsup0  31068  spansnpji  31098  mayetes3i  31249  nlelshi  31580  pjimai  31696  pj3i  31728  shatomistici  31881  hatomistici  31882  atcvat4i  31917  iundisjf  32087  rinvf1o  32121  mptctf  32209  iundisjfi  32274  xrge0mulgnn0  32457  gsumpart  32477  fermltlchr  32752  znfermltl  32753  ply1degltel  32940  ply1degleel  32941  ply1degltlss  32942  ccfldsrarelvec  33034  ccfldextdgrr  33035  xrge0iifcnv  33211  xrge0iifiso  33213  xrge0iifhom  33215  esumcvgsum  33384  coinfliprv  33779  signsply0  33860  signstcl  33874  signstf  33875  kur14lem6  34500  mthmsta  34867  gg-psercn2  35464  filnetlem3  35568  filnetlem4  35569  onint1  35637  oninhaus  35638  bj-nuliotaALT  36242  imadifss  36766  poimirlem3  36794  poimirlem32  36823  dvtan  36841  itg2addnclem2  36843  ftc1anclem6  36869  heiborlem3  36984  isdrngo2  37129  elrfi  41734  mapfzcons1  41757  eldioph4b  41851  dnnumch3lem  42090  dnnumch3  42091  dgraalem  42189  dgraaub  42192  resnonrel  42645  cotrcltrcl  42778  cotrclrcl  42795  frege131d  42817  binomcxplemdvbinom  43414  binomcxplemdvsum  43416  binomcxplemnotnn0  43417  relopabVD  43964  rabexgf  44010  fzssnn0  44325  iuneqfzuzlem  44342  allbutfiinf  44428  uzublem  44438  sumnnodd  44644  lptioo2cn  44659  lptioo1cn  44660  fourierdlem31  45152  fourierdlem102  45222  fourierdlem114  45234  fouriercn  45246  elaa2lem  45247  etransclem48  45296  salexct  45348  salgencntex  45357  sge0resplit  45420  meaiuninclem  45494  caratheodorylem1  45540  hoicvr  45562  hoicvrrex  45570  hoidmvlelem3  45611  hoidmvlelem4  45612