Theorem sseqtri 3924

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

Syntax hints:   = wceq 1522   ⊆ wss 3859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-in 3866  df-ss 3874

This theorem is referenced by:  sseqtr4i  3925  eqimssi  3946  abssi  3967  ssun2  4070  unixpss  5569  0ima  5822  fvssunirn  6567  mptexgf  6851  difex2  7339  oelim2  8071  omopthlem2  8133  sbthlem7  8480  unifpw  8673  fiuni  8738  rankuni  9138  rankc2  9146  rankxpu  9151  rankmapu  9153  rankxplim  9154  infxpenlem  9285  cf0  9519  fin23lem17  9606  fin23lem31  9611  smobeth  9854  nqerf  10198  dmrecnq  10236  ackbijnn  15016  divalglem2  15579  divalglem5  15581  bitsfzolem  15616  0bits  15621  bezoutlem2  15717  bezoutlem3  15718  lcmcllem  15769  lcmledvds  15772  lcmfval  15794  lcmfcllem  15798  lcmfledvds  15805  odzcllem  15958  odzdvds  15961  unbenlem  16073  4sqlem13  16122  4sqlem14  16123  4sqlem17  16126  4sqlem18  16127  vdwlem8  16153  vdwnnlem3  16162  ramcl2lem  16174  ramtcl  16175  ramtub  16177  strle1  16421  prdsval  16557  wunfunc  16998  wunnat  17055  psssdm2  17654  tsrss  17662  gicer  18157  symgsssg  18326  symgfisg  18327  odfval  18391  odlem2  18398  gexlem2  18437  torsubg  18697  dprd2da  18881  zringlpirlem2  20314  zringlpirlem3  20315  pjfval  20532  pjpm  20534  toponsspwpw  21214  eltg4i  21252  ntrss2  21349  isopn3  21358  mretopd  21384  leordtval2  21504  ptbasfi  21873  hmphtop  22070  hmpher  22076  restutop  22529  ucnprima  22574  tngtopn  22942  tgioo  23087  xrtgioo  23097  ovolicc2lem4  23804  nulmbl2  23820  iundisj  23832  dyadmax  23882  i1f1  23974  dvfval  24178  dvcnp2  24200  lhop1lem  24293  lhop2  24295  elqaalem1  24591  elqaalem3  24593  taylthlem2  24645  pserulm  24693  psercn2  24694  psercnlem2  24695  psercnlem1  24696  psercn  24697  pserdvlem1  24698  pserdvlem2  24699  pserdv  24700  pserdv2  24701  abelth  24712  dvlog  24915  efopnlem2  24921  logtayl  24924  cxpcn3lem  25009  cxpcn3  25010  resqrtcn  25011  dvatan  25194  atancn  25195  rlimcnp  25225  rlimcnp2  25226  wilthlem3  25329  ftalem4  25335  ftalem5  25336  dchrisum0lem2a  25775  cchhllem  26356  axlowdimlem6  26416  hhssabloilem  28729  choc1  28795  chub2i  28938  span0  29010  spanuni  29012  sshhococi  29014  chsup0  29016  spansnpji  29046  mayetes3i  29197  nlelshi  29528  pjimai  29644  pj3i  29676  shatomistici  29829  hatomistici  29830  atcvat4i  29865  iundisjf  30029  rinvf1o  30065  mptctf  30141  iundisjfi  30205  xrge0mulgnn0  30350  ccfldsrarelvec  30660  ccfldextdgrr  30661  xrge0iifcnv  30793  xrge0iifiso  30795  xrge0iifhom  30797  esumcvgsum  30964  coinfliprv  31357  signsply0  31438  signstcl  31452  signstf  31453  kur14lem6  32066  mthmsta  32433  bdayimaon  32806  nosupbday  32814  noetalem3  32828  noetalem4  32829  nocvxminlem  32856  nocvxmin  32857  filnetlem3  33337  filnetlem4  33338  onint1  33406  oninhaus  33407  bj-nuliotaALT  33949  imadifss  34398  poimirlem3  34426  poimirlem32  34455  dvtan  34473  itg2addnclem2  34475  ftc1anclem6  34503  heiborlem3  34623  isdrngo2  34768  elrfi  38776  mapfzcons1  38799  eldioph4b  38893  dnnumch3lem  39131  dnnumch3  39132  dgraalem  39230  dgraaub  39233  resnonrel  39437  cotrcltrcl  39555  cotrclrcl  39572  frege131d  39594  binomcxplemdvbinom  40223  binomcxplemdvsum  40225  binomcxplemnotnn0  40226  relopabVD  40774  rabexgf  40820  fzssnn0  41126  iuneqfzuzlem  41143  allbutfiinf  41236  uzublem  41246  sumnnodd  41453  lptioo2cn  41468  lptioo1cn  41469  fourierdlem31  41965  fourierdlem102  42035  fourierdlem114  42047  fouriercn  42059  elaa2lem  42060  etransclem48  42109  salexct  42159  salgencntex  42168  sge0resplit  42230  meaiuninclem  42304  caratheodorylem1  42350  hoicvr  42372  hoicvrrex  42380  hoidmvlelem3  42421  hoidmvlelem4  42422