Theorem sseqtri 3828

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

Syntax hints:   = wceq 1637   ⊆ wss 3763

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2067  ax-7 2103  ax-9 2164  ax-10 2184  ax-11 2200  ax-12 2213  ax-ext 2781

This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2060  df-clab 2789  df-cleq 2795  df-clel 2798  df-in 3770  df-ss 3777

This theorem is referenced by:  sseqtr4i  3829  eqimssi  3850  abssi  3868  ssun2  3970  unixpss  5429  0ima  5686  idssxpOLD  6214  fvssunirn  6431  mptexgf  6704  difex2  7193  oelim2  7906  omopthlem2  7967  sbthlem7  8309  unifpw  8502  fiuni  8567  rankuni  8967  rankc2  8975  rankxpu  8980  rankmapu  8982  rankxplim  8983  infxpenlem  9113  cf0  9352  fin23lem17  9439  fin23lem31  9444  smobeth  9687  nqerf  10031  dmrecnq  10069  ackbijnn  14776  divalglem2  15332  divalglem5  15334  bitsfzolem  15369  0bits  15374  bezoutlem2  15470  bezoutlem3  15471  lcmcllem  15522  lcmledvds  15525  lcmfval  15547  lcmfcllem  15551  lcmfledvds  15558  odzcllem  15708  odzdvds  15711  unbenlem  15823  4sqlem13  15872  4sqlem14  15873  4sqlem17  15876  4sqlem18  15877  vdwlem8  15903  vdwnnlem3  15912  ramcl2lem  15924  ramtcl  15925  ramtub  15927  strle1  16178  prdsval  16314  xpsc0  16419  xpsc1  16420  wunfunc  16757  wunnat  16814  psssdm2  17414  tsrss  17422  gicer  17914  symgsssg  18082  symgfisg  18083  odlem2  18153  gexlem2  18192  torsubg  18452  dprd2da  18637  zringlpirlem2  20035  zringlpirlem3  20036  pjfval  20254  pjpm  20256  toponsspwpw  20934  eltg4i  20972  ntrss2  21069  isopn3  21078  mretopd  21104  leordtval2  21224  ptbasfi  21592  hmphtop  21789  hmpher  21795  restutop  22248  ucnprima  22293  tngtopn  22661  tgioo  22806  xrtgioo  22816  ovolicc2lem4  23495  nulmbl2  23511  iundisj  23523  dyadmax  23573  i1f1  23665  dvfval  23869  dvcnp2  23891  lhop1lem  23984  lhop2  23986  elqaalem1  24282  elqaalem3  24284  taylthlem2  24336  pserulm  24384  psercn2  24385  psercnlem2  24386  psercnlem1  24387  psercn  24388  pserdvlem1  24389  pserdvlem2  24390  pserdv  24391  pserdv2  24392  abelth  24403  dvlog  24605  efopnlem2  24611  logtayl  24614  cxpcn3lem  24696  cxpcn3  24697  resqrtcn  24698  dvatan  24870  atancn  24871  rlimcnp  24900  rlimcnp2  24901  wilthlem3  25004  ftalem4  25010  ftalem5  25011  dchrisum0lem2a  25414  cchhllem  25975  axlowdimlem6  26035  hhssabloilem  28440  choc1  28508  chub2i  28651  span0  28723  spanuni  28725  sshhococi  28727  chsup0  28729  spansnpji  28759  mayetes3i  28910  nlelshi  29241  pjimai  29357  pj3i  29389  shatomistici  29542  hatomistici  29543  atcvat4i  29578  iundisjf  29721  rinvf1o  29753  mptctf  29816  iundisjfi  29876  xrge0mulgnn0  30008  xrge0iifcnv  30298  xrge0iifiso  30300  xrge0iifhom  30302  esumcvgsum  30469  coinfliprv  30863  signsply0  30947  signstcl  30961  signstf  30962  kur14lem6  31510  mthmsta  31792  bdayimaon  32158  nosupbday  32166  noetalem3  32180  noetalem4  32181  nocvxminlem  32208  nocvxmin  32209  filnetlem3  32690  filnetlem4  32691  onint1  32759  oninhaus  32760  bj-nuliotaALT  33324  imadifss  33691  poimirlem3  33719  poimirlem32  33748  dvtan  33766  itg2addnclem2  33768  ftc1anclem6  33796  heiborlem3  33917  isdrngo2  34062  elrfi  37753  mapfzcons1  37776  eldioph4b  37871  dnnumch3lem  38111  dnnumch3  38112  dgraalem  38210  dgraaub  38213  resnonrel  38392  rtrclex  38418  rtrclexi  38422  cotrcltrcl  38511  cotrclrcl  38528  frege131d  38550  binomcxplemdvbinom  39046  binomcxplemdvsum  39048  binomcxplemnotnn0  39049  relopabVD  39625  rabexgf  39671  fzssnn0  40007  iuneqfzuzlem  40024  allbutfiinf  40120  uzublem  40130  sumnnodd  40336  lptioo2cn  40351  lptioo1cn  40352  fourierdlem31  40828  fourierdlem102  40898  fourierdlem114  40910  fouriercn  40922  elaa2lem  40923  etransclem48  40972  salexct  41025  salgencntex  41034  sge0resplit  41096  meaiuninclem  41170  caratheodorylem1  41216  hoicvr  41238  hoicvrrex  41246  hoidmvlelem3  41287  hoidmvlelem4  41288