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 1541   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3951  df-ss 3961

This theorem is referenced by:  sseqtrri  4015  eqimssi  4038  abssi  4063  ssun2  4169  unixpss  5802  0ima  6066  fvssunirnOLD  6912  mptexgf  7208  difex2  7730  oelim2  8578  omopthlem2  8642  sbthlem7  9072  unifpw  9338  fiuni  9405  dmttrcl  9698  rnttrcl  9699  ttrclexg  9700  rankuni  9840  rankc2  9848  rankxpu  9853  rankmapu  9855  rankxplim  9856  infxpenlem  9990  cf0  10228  fin23lem17  10315  fin23lem31  10320  smobeth  10563  nqerf  10907  dmrecnq  10945  ackbijnn  15756  divalglem2  16320  divalglem5  16322  bitsfzolem  16357  0bits  16362  bezoutlem2  16464  bezoutlem3  16465  lcmcllem  16515  lcmledvds  16518  lcmfval  16540  lcmfcllem  16544  lcmfledvds  16551  odzcllem  16707  odzdvds  16710  unbenlem  16823  4sqlem13  16872  4sqlem14  16873  4sqlem17  16876  4sqlem18  16877  vdwlem8  16903  vdwnnlem3  16912  ramcl2lem  16924  ramtcl  16925  ramtub  16927  strle1  17073  prdsvallem  17382  wunfunc  17831  wunfuncOLD  17832  wunnat  17889  wunnatOLD  17890  psssdm2  18516  tsrss  18524  gicer  19116  symgsssg  19299  symgfisg  19300  odfval  19364  odlem2  19371  gexlem2  19414  torsubg  19682  dprd2da  19871  zringlpirlem2  20966  zringlpirlem3  20967  pjfval  21194  pjpm  21196  toponsspwpw  22353  eltg4i  22392  ntrss2  22490  isopn3  22499  mretopd  22525  leordtval2  22645  ptbasfi  23014  hmphtop  23211  hmpher  23217  restutop  23671  ucnprima  23716  tngtopn  24096  tgioo  24241  xrtgioo  24251  ovolicc2lem4  24966  nulmbl2  24982  iundisj  24994  dyadmax  25044  i1f1  25136  dvfval  25343  dvcnp2  25366  lhop1lem  25459  lhop2  25461  elqaalem1  25761  elqaalem3  25763  taylthlem2  25815  pserulm  25863  psercn2  25864  psercnlem2  25865  psercnlem1  25866  psercn  25867  pserdvlem1  25868  pserdvlem2  25869  pserdv  25870  pserdv2  25871  abelth  25882  dvlog  26088  efopnlem2  26094  logtayl  26097  cxpcn3lem  26182  cxpcn3  26183  resqrtcn  26184  dvatan  26367  atancn  26368  rlimcnp  26397  rlimcnp2  26398  wilthlem3  26501  ftalem4  26507  ftalem5  26508  dchrisum0lem2a  26947  bdayimaon  27123  noetasuplem4  27166  noetainflem4  27170  nocvxminlem  27205  nocvxmin  27206  noeta2  27212  etasslt2  27241  scutbdaybnd2lim  27244  bday1s  27258  lrrecfr  27343  negsunif  27443  cchhllem  28009  cchhllemOLD  28010  axlowdimlem6  28070  hhssabloilem  30377  choc1  30443  chub2i  30586  span0  30658  spanuni  30660  sshhococi  30662  chsup0  30664  spansnpji  30694  mayetes3i  30845  nlelshi  31176  pjimai  31292  pj3i  31324  shatomistici  31477  hatomistici  31478  atcvat4i  31513  iundisjf  31685  rinvf1o  31722  mptctf  31813  iundisjfi  31878  xrge0mulgnn0  32061  gsumpart  32078  fermltlchr  32340  znfermltl  32341  ply1degltel  32506  ply1degltlss  32507  ccfldsrarelvec  32583  ccfldextdgrr  32584  xrge0iifcnv  32744  xrge0iifiso  32746  xrge0iifhom  32748  esumcvgsum  32917  coinfliprv  33312  signsply0  33393  signstcl  33407  signstf  33408  kur14lem6  34033  mthmsta  34400  filnetlem3  35069  filnetlem4  35070  onint1  35138  oninhaus  35139  bj-nuliotaALT  35743  imadifss  36267  poimirlem3  36295  poimirlem32  36324  dvtan  36342  itg2addnclem2  36344  ftc1anclem6  36370  heiborlem3  36486  isdrngo2  36631  elrfi  41203  mapfzcons1  41226  eldioph4b  41320  dnnumch3lem  41559  dnnumch3  41560  dgraalem  41658  dgraaub  41661  resnonrel  42114  cotrcltrcl  42247  cotrclrcl  42264  frege131d  42286  binomcxplemdvbinom  42883  binomcxplemdvsum  42885  binomcxplemnotnn0  42886  relopabVD  43433  rabexgf  43479  fzssnn0  43800  iuneqfzuzlem  43817  allbutfiinf  43903  uzublem  43913  sumnnodd  44119  lptioo2cn  44134  lptioo1cn  44135  fourierdlem31  44627  fourierdlem102  44697  fourierdlem114  44709  fouriercn  44721  elaa2lem  44722  etransclem48  44771  salexct  44823  salgencntex  44832  sge0resplit  44895  meaiuninclem  44969  caratheodorylem1  45015  hoicvr  45037  hoicvrrex  45045  hoidmvlelem3  45086  hoidmvlelem4  45087