Theorem sseqtri 4045

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

Syntax hints:   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  sseqtrri  4046  eqimssi  4069  abssi  4093  ssun2  4202  unixpss  5834  0ima  6107  fvssunirnOLD  6954  mptexgf  7259  difex2  7795  oelim2  8651  omopthlem2  8716  sbthlem7  9155  unifpw  9425  fiuni  9497  dmttrcl  9790  rnttrcl  9791  ttrclexg  9792  rankuni  9932  rankc2  9940  rankxpu  9945  rankmapu  9947  rankxplim  9948  infxpenlem  10082  cf0  10320  fin23lem17  10407  fin23lem31  10412  smobeth  10655  nqerf  10999  dmrecnq  11037  ackbijnn  15876  divalglem2  16443  divalglem5  16445  bitsfzolem  16480  0bits  16485  bezoutlem2  16587  bezoutlem3  16588  lcmcllem  16643  lcmledvds  16646  lcmfval  16668  lcmfcllem  16672  lcmfledvds  16679  odzcllem  16839  odzdvds  16842  unbenlem  16955  4sqlem13  17004  4sqlem14  17005  4sqlem17  17008  4sqlem18  17009  vdwlem8  17035  vdwnnlem3  17044  ramcl2lem  17056  ramtcl  17057  ramtub  17059  strle1  17205  prdsvallem  17514  wunfunc  17965  wunfuncOLD  17966  wunnat  18024  wunnatOLD  18025  psssdm2  18651  tsrss  18659  gicer  19317  symgsssg  19509  symgfisg  19510  odfval  19574  odlem2  19581  gexlem2  19624  torsubg  19896  dprd2da  20086  zringlpirlem2  21497  zringlpirlem3  21498  fermltlchr  21567  pjfval  21749  pjpm  21751  toponsspwpw  22949  eltg4i  22988  ntrss2  23086  isopn3  23095  mretopd  23121  leordtval2  23241  ptbasfi  23610  hmphtop  23807  hmpher  23813  restutop  24267  ucnprima  24312  tngtopn  24692  tgioo  24837  xrtgioo  24847  ovolicc2lem4  25574  nulmbl2  25590  iundisj  25602  dyadmax  25652  i1f1  25744  dvfval  25952  dvcnp2  25975  dvcnp2OLD  25976  lhop1lem  26072  lhop2  26074  elqaalem1  26379  elqaalem3  26381  taylthlem2  26434  taylthlem2OLD  26435  pserulm  26483  psercn2  26484  psercn2OLD  26485  psercnlem2  26486  psercnlem1  26487  psercn  26488  pserdvlem1  26489  pserdvlem2  26490  pserdv  26491  pserdv2  26492  abelth  26503  dvlog  26711  efopnlem2  26717  logtayl  26720  cxpcn3lem  26808  cxpcn3  26809  resqrtcn  26810  dvatan  26996  atancn  26997  rlimcnp  27026  rlimcnp2  27027  wilthlem3  27131  ftalem4  27137  ftalem5  27138  dchrisum0lem2a  27579  bdayimaon  27756  noetasuplem4  27799  noetainflem4  27803  nocvxminlem  27840  nocvxmin  27841  noeta2  27847  etasslt2  27877  scutbdaybnd2lim  27880  bday1s  27894  lrrecfr  27994  addsbdaylem  28067  negsunif  28105  zs12bday  28442  cchhllem  28919  cchhllemOLD  28920  axlowdimlem6  28980  hhssabloilem  31293  choc1  31359  chub2i  31502  span0  31574  spanuni  31576  sshhococi  31578  chsup0  31580  spansnpji  31610  mayetes3i  31761  nlelshi  32092  pjimai  32208  pj3i  32240  shatomistici  32393  hatomistici  32394  atcvat4i  32429  iundisjf  32611  rinvf1o  32649  mptctf  32731  iundisjfi  32801  xrge0mulgnn0  33001  gsumpart  33038  znfermltl  33359  ply1degltel  33580  ply1degleel  33581  ply1degltlss  33582  ccfldsrarelvec  33681  ccfldextdgrr  33682  2sqr3minply  33738  xrge0iifcnv  33879  xrge0iifiso  33881  xrge0iifhom  33883  esumcvgsum  34052  coinfliprv  34447  signsply0  34528  signstcl  34542  signstf  34543  kur14lem6  35179  mthmsta  35546  filnetlem3  36346  filnetlem4  36347  onint1  36415  oninhaus  36416  bj-nuliotaALT  37024  imadifss  37555  poimirlem3  37583  poimirlem32  37612  dvtan  37630  itg2addnclem2  37632  ftc1anclem6  37658  heiborlem3  37773  isdrngo2  37918  elrfi  42650  mapfzcons1  42673  eldioph4b  42767  dnnumch3lem  43003  dnnumch3  43004  dgraalem  43102  dgraaub  43105  resnonrel  43554  cotrcltrcl  43687  cotrclrcl  43704  frege131d  43726  binomcxplemdvbinom  44322  binomcxplemdvsum  44324  binomcxplemnotnn0  44325  relopabVD  44872  rabexgf  44924  fzssnn0  45232  iuneqfzuzlem  45249  allbutfiinf  45335  uzublem  45345  sumnnodd  45551  lptioo2cn  45566  lptioo1cn  45567  fourierdlem31  46059  fourierdlem102  46129  fourierdlem114  46141  fouriercn  46153  elaa2lem  46154  etransclem48  46203  salexct  46255  salgencntex  46264  sge0resplit  46327  meaiuninclem  46401  caratheodorylem1  46447  hoicvr  46469  hoicvrrex  46477  hoidmvlelem3  46518  hoidmvlelem4  46519  gricrel  47772  grlicrel  47823