Theorem sseqtri 3923

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

Syntax hints:   = wceq 1543   ⊆ wss 3853

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2073  df-clab 2715  df-cleq 2728  df-clel 2809  df-v 3400  df-in 3860  df-ss 3870

This theorem is referenced by:  sseqtrri  3924  eqimssi  3945  abssi  3969  ssun2  4073  unixpss  5665  0ima  5931  fvssunirn  6724  mptexgf  7016  difex2  7523  oelim2  8301  omopthlem2  8363  sbthlem7  8740  unifpw  8957  fiuni  9022  rankuni  9444  rankc2  9452  rankxpu  9457  rankmapu  9459  rankxplim  9460  infxpenlem  9592  cf0  9830  fin23lem17  9917  fin23lem31  9922  smobeth  10165  nqerf  10509  dmrecnq  10547  ackbijnn  15355  divalglem2  15919  divalglem5  15921  bitsfzolem  15956  0bits  15961  bezoutlem2  16063  bezoutlem3  16064  lcmcllem  16116  lcmledvds  16119  lcmfval  16141  lcmfcllem  16145  lcmfledvds  16152  odzcllem  16308  odzdvds  16311  unbenlem  16424  4sqlem13  16473  4sqlem14  16474  4sqlem17  16477  4sqlem18  16478  vdwlem8  16504  vdwnnlem3  16513  ramcl2lem  16525  ramtcl  16526  ramtub  16528  strle1  16776  prdsvallem  16913  wunfunc  17359  wunfuncOLD  17360  wunnat  17417  wunnatOLD  17418  psssdm2  18041  tsrss  18049  gicer  18634  symgsssg  18813  symgfisg  18814  odfval  18878  odlem2  18885  gexlem2  18925  torsubg  19193  dprd2da  19383  zringlpirlem2  20404  zringlpirlem3  20405  pjfval  20622  pjpm  20624  toponsspwpw  21773  eltg4i  21811  ntrss2  21908  isopn3  21917  mretopd  21943  leordtval2  22063  ptbasfi  22432  hmphtop  22629  hmpher  22635  restutop  23089  ucnprima  23133  tngtopn  23502  tgioo  23647  xrtgioo  23657  ovolicc2lem4  24371  nulmbl2  24387  iundisj  24399  dyadmax  24449  i1f1  24541  dvfval  24748  dvcnp2  24771  lhop1lem  24864  lhop2  24866  elqaalem1  25166  elqaalem3  25168  taylthlem2  25220  pserulm  25268  psercn2  25269  psercnlem2  25270  psercnlem1  25271  psercn  25272  pserdvlem1  25273  pserdvlem2  25274  pserdv  25275  pserdv2  25276  abelth  25287  dvlog  25493  efopnlem2  25499  logtayl  25502  cxpcn3lem  25587  cxpcn3  25588  resqrtcn  25589  dvatan  25772  atancn  25773  rlimcnp  25802  rlimcnp2  25803  wilthlem3  25906  ftalem4  25912  ftalem5  25913  dchrisum0lem2a  26352  cchhllem  26932  axlowdimlem6  26992  hhssabloilem  29296  choc1  29362  chub2i  29505  span0  29577  spanuni  29579  sshhococi  29581  chsup0  29583  spansnpji  29613  mayetes3i  29764  nlelshi  30095  pjimai  30211  pj3i  30243  shatomistici  30396  hatomistici  30397  atcvat4i  30432  iundisjf  30601  rinvf1o  30638  mptctf  30726  iundisjfi  30791  xrge0mulgnn0  30971  gsumpart  30988  znfermltl  31230  ccfldsrarelvec  31409  ccfldextdgrr  31410  xrge0iifcnv  31551  xrge0iifiso  31553  xrge0iifhom  31555  esumcvgsum  31722  coinfliprv  32115  signsply0  32196  signstcl  32210  signstf  32211  kur14lem6  32840  mthmsta  33207  bdayimaon  33582  noetasuplem4  33625  noetainflem4  33629  nocvxminlem  33658  nocvxmin  33659  noeta2  33665  etasslt2  33694  scutbdaybnd2lim  33697  bday1s  33711  lrrecfr  33786  filnetlem3  34255  filnetlem4  34256  onint1  34324  oninhaus  34325  bj-nuliotaALT  34915  imadifss  35438  poimirlem3  35466  poimirlem32  35495  dvtan  35513  itg2addnclem2  35515  ftc1anclem6  35541  heiborlem3  35657  isdrngo2  35802  elrfi  40160  mapfzcons1  40183  eldioph4b  40277  dnnumch3lem  40515  dnnumch3  40516  dgraalem  40614  dgraaub  40617  resnonrel  40817  cotrcltrcl  40951  cotrclrcl  40968  frege131d  40990  binomcxplemdvbinom  41585  binomcxplemdvsum  41587  binomcxplemnotnn0  41588  relopabVD  42135  rabexgf  42181  fzssnn0  42470  iuneqfzuzlem  42487  allbutfiinf  42574  uzublem  42584  sumnnodd  42789  lptioo2cn  42804  lptioo1cn  42805  fourierdlem31  43297  fourierdlem102  43367  fourierdlem114  43379  fouriercn  43391  elaa2lem  43392  etransclem48  43441  salexct  43491  salgencntex  43500  sge0resplit  43562  meaiuninclem  43636  caratheodorylem1  43682  hoicvr  43704  hoicvrrex  43712  hoidmvlelem3  43753  hoidmvlelem4  43754