Theorem sseqtri 3968

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

Syntax hints:   = wceq 1540   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915

This theorem is referenced by:  sseqtrri  3969  eqimssi  3990  abssi  4015  ssun2  4120  unixpss  5752  0ima  6016  fvssunirnOLD  6859  mptexgf  7154  difex2  7672  oelim2  8497  omopthlem2  8561  sbthlem7  8954  unifpw  9220  fiuni  9285  dmttrcl  9578  rnttrcl  9579  ttrclexg  9580  rankuni  9720  rankc2  9728  rankxpu  9733  rankmapu  9735  rankxplim  9736  infxpenlem  9870  cf0  10108  fin23lem17  10195  fin23lem31  10200  smobeth  10443  nqerf  10787  dmrecnq  10825  ackbijnn  15639  divalglem2  16203  divalglem5  16205  bitsfzolem  16240  0bits  16245  bezoutlem2  16347  bezoutlem3  16348  lcmcllem  16398  lcmledvds  16401  lcmfval  16423  lcmfcllem  16427  lcmfledvds  16434  odzcllem  16590  odzdvds  16593  unbenlem  16706  4sqlem13  16755  4sqlem14  16756  4sqlem17  16759  4sqlem18  16760  vdwlem8  16786  vdwnnlem3  16795  ramcl2lem  16807  ramtcl  16808  ramtub  16810  strle1  16956  prdsvallem  17262  wunfunc  17711  wunfuncOLD  17712  wunnat  17769  wunnatOLD  17770  psssdm2  18396  tsrss  18404  gicer  18988  symgsssg  19171  symgfisg  19172  odfval  19236  odlem2  19243  gexlem2  19283  torsubg  19550  dprd2da  19740  zringlpirlem2  20791  zringlpirlem3  20792  pjfval  21019  pjpm  21021  toponsspwpw  22177  eltg4i  22216  ntrss2  22314  isopn3  22323  mretopd  22349  leordtval2  22469  ptbasfi  22838  hmphtop  23035  hmpher  23041  restutop  23495  ucnprima  23540  tngtopn  23920  tgioo  24065  xrtgioo  24075  ovolicc2lem4  24790  nulmbl2  24806  iundisj  24818  dyadmax  24868  i1f1  24960  dvfval  25167  dvcnp2  25190  lhop1lem  25283  lhop2  25285  elqaalem1  25585  elqaalem3  25587  taylthlem2  25639  pserulm  25687  psercn2  25688  psercnlem2  25689  psercnlem1  25690  psercn  25691  pserdvlem1  25692  pserdvlem2  25693  pserdv  25694  pserdv2  25695  abelth  25706  dvlog  25912  efopnlem2  25918  logtayl  25921  cxpcn3lem  26006  cxpcn3  26007  resqrtcn  26008  dvatan  26191  atancn  26192  rlimcnp  26221  rlimcnp2  26222  wilthlem3  26325  ftalem4  26331  ftalem5  26332  dchrisum0lem2a  26771  bdayimaon  26947  noetasuplem4  26990  noetainflem4  26994  nocvxminlem  27023  nocvxmin  27024  noeta2  27030  etasslt2  27059  scutbdaybnd2lim  27062  bday1s  27076  cchhllem  27543  cchhllemOLD  27544  axlowdimlem6  27604  hhssabloilem  29911  choc1  29977  chub2i  30120  span0  30192  spanuni  30194  sshhococi  30196  chsup0  30198  spansnpji  30228  mayetes3i  30379  nlelshi  30710  pjimai  30826  pj3i  30858  shatomistici  31011  hatomistici  31012  atcvat4i  31047  iundisjf  31215  rinvf1o  31252  mptctf  31339  iundisjfi  31404  xrge0mulgnn0  31585  gsumpart  31602  fermltlchr  31858  znfermltl  31859  ccfldsrarelvec  32039  ccfldextdgrr  32040  xrge0iifcnv  32181  xrge0iifiso  32183  xrge0iifhom  32185  esumcvgsum  32354  coinfliprv  32749  signsply0  32830  signstcl  32844  signstf  32845  kur14lem6  33472  mthmsta  33839  lrrecfr  34196  filnetlem3  34665  filnetlem4  34666  onint1  34734  oninhaus  34735  bj-nuliotaALT  35342  imadifss  35865  poimirlem3  35893  poimirlem32  35922  dvtan  35940  itg2addnclem2  35942  ftc1anclem6  35968  heiborlem3  36084  isdrngo2  36229  elrfi  40786  mapfzcons1  40809  eldioph4b  40903  dnnumch3lem  41142  dnnumch3  41143  dgraalem  41241  dgraaub  41244  resnonrel  41529  cotrcltrcl  41662  cotrclrcl  41679  frege131d  41701  binomcxplemdvbinom  42300  binomcxplemdvsum  42302  binomcxplemnotnn0  42303  relopabVD  42850  rabexgf  42896  fzssnn0  43199  iuneqfzuzlem  43216  allbutfiinf  43303  uzublem  43313  sumnnodd  43515  lptioo2cn  43530  lptioo1cn  43531  fourierdlem31  44023  fourierdlem102  44093  fourierdlem114  44105  fouriercn  44117  elaa2lem  44118  etransclem48  44167  salexct  44217  salgencntex  44226  sge0resplit  44289  meaiuninclem  44363  caratheodorylem1  44409  hoicvr  44431  hoicvrrex  44439  hoidmvlelem3  44480  hoidmvlelem4  44481