Theorem sseqtri 4014

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

Syntax hints:   = wceq 1533   ⊆ wss 3945

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ss 3962

This theorem is referenced by:  sseqtrri  4015  eqimssi  4038  abssi  4064  ssun2  4172  unixpss  5811  0ima  6081  fvssunirnOLD  6928  mptexgf  7232  difex2  7761  oelim2  8614  omopthlem2  8679  sbthlem7  9112  unifpw  9379  fiuni  9451  dmttrcl  9744  rnttrcl  9745  ttrclexg  9746  rankuni  9886  rankc2  9894  rankxpu  9899  rankmapu  9901  rankxplim  9902  infxpenlem  10036  cf0  10274  fin23lem17  10361  fin23lem31  10366  smobeth  10609  nqerf  10953  dmrecnq  10991  ackbijnn  15806  divalglem2  16371  divalglem5  16373  bitsfzolem  16408  0bits  16413  bezoutlem2  16515  bezoutlem3  16516  lcmcllem  16566  lcmledvds  16569  lcmfval  16591  lcmfcllem  16595  lcmfledvds  16602  odzcllem  16760  odzdvds  16763  unbenlem  16876  4sqlem13  16925  4sqlem14  16926  4sqlem17  16929  4sqlem18  16930  vdwlem8  16956  vdwnnlem3  16965  ramcl2lem  16977  ramtcl  16978  ramtub  16980  strle1  17126  prdsvallem  17435  wunfunc  17886  wunfuncOLD  17887  wunnat  17945  wunnatOLD  17946  psssdm2  18572  tsrss  18580  gicer  19235  symgsssg  19426  symgfisg  19427  odfval  19491  odlem2  19498  gexlem2  19541  torsubg  19813  dprd2da  20003  zringlpirlem2  21393  zringlpirlem3  21394  fermltlchr  21463  pjfval  21644  pjpm  21646  toponsspwpw  22854  eltg4i  22893  ntrss2  22991  isopn3  23000  mretopd  23026  leordtval2  23146  ptbasfi  23515  hmphtop  23712  hmpher  23718  restutop  24172  ucnprima  24217  tngtopn  24597  tgioo  24742  xrtgioo  24752  ovolicc2lem4  25479  nulmbl2  25495  iundisj  25507  dyadmax  25557  i1f1  25649  dvfval  25856  dvcnp2  25879  dvcnp2OLD  25880  lhop1lem  25976  lhop2  25978  elqaalem1  26284  elqaalem3  26286  taylthlem2  26339  taylthlem2OLD  26340  pserulm  26388  psercn2  26389  psercn2OLD  26390  psercnlem2  26391  psercnlem1  26392  psercn  26393  pserdvlem1  26394  pserdvlem2  26395  pserdv  26396  pserdv2  26397  abelth  26408  dvlog  26615  efopnlem2  26621  logtayl  26624  cxpcn3lem  26712  cxpcn3  26713  resqrtcn  26714  dvatan  26897  atancn  26898  rlimcnp  26927  rlimcnp2  26928  wilthlem3  27032  ftalem4  27038  ftalem5  27039  dchrisum0lem2a  27480  bdayimaon  27656  noetasuplem4  27699  noetainflem4  27703  nocvxminlem  27740  nocvxmin  27741  noeta2  27747  etasslt2  27777  scutbdaybnd2lim  27780  bday1s  27794  lrrecfr  27890  negsunif  27997  cchhllem  28753  cchhllemOLD  28754  axlowdimlem6  28814  hhssabloilem  31127  choc1  31193  chub2i  31336  span0  31408  spanuni  31410  sshhococi  31412  chsup0  31414  spansnpji  31444  mayetes3i  31595  nlelshi  31926  pjimai  32042  pj3i  32074  shatomistici  32227  hatomistici  32228  atcvat4i  32263  iundisjf  32436  rinvf1o  32472  mptctf  32556  iundisjfi  32621  xrge0mulgnn0  32802  gsumpart  32826  znfermltl  33138  ply1degltel  33335  ply1degleel  33336  ply1degltlss  33337  ccfldsrarelvec  33429  ccfldextdgrr  33430  xrge0iifcnv  33604  xrge0iifiso  33606  xrge0iifhom  33608  esumcvgsum  33777  coinfliprv  34172  signsply0  34253  signstcl  34267  signstf  34268  kur14lem6  34891  mthmsta  35258  filnetlem3  35934  filnetlem4  35935  onint1  36003  oninhaus  36004  bj-nuliotaALT  36607  imadifss  37138  poimirlem3  37166  poimirlem32  37195  dvtan  37213  itg2addnclem2  37215  ftc1anclem6  37241  heiborlem3  37356  isdrngo2  37501  elrfi  42179  mapfzcons1  42202  eldioph4b  42296  dnnumch3lem  42535  dnnumch3  42536  dgraalem  42634  dgraaub  42637  resnonrel  43087  cotrcltrcl  43220  cotrclrcl  43237  frege131d  43259  binomcxplemdvbinom  43855  binomcxplemdvsum  43857  binomcxplemnotnn0  43858  relopabVD  44405  rabexgf  44451  fzssnn0  44762  iuneqfzuzlem  44779  allbutfiinf  44865  uzublem  44875  sumnnodd  45081  lptioo2cn  45096  lptioo1cn  45097  fourierdlem31  45589  fourierdlem102  45659  fourierdlem114  45671  fouriercn  45683  elaa2lem  45684  etransclem48  45733  salexct  45785  salgencntex  45794  sge0resplit  45857  meaiuninclem  45931  caratheodorylem1  45977  hoicvr  45999  hoicvrrex  46007  hoidmvlelem3  46048  hoidmvlelem4  46049  gricrel  47297