Theorem sseqtri 4002

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

Syntax hints:   = wceq 1533   ⊆ wss 3935

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1907  ax-6 1966  ax-7 2011  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2157  ax-12 2173  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1536  df-ex 1777  df-nf 1781  df-sb 2066  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3942  df-ss 3951

This theorem is referenced by:  sseqtrri  4003  eqimssi  4024  abssi  4045  ssun2  4148  unixpss  5677  0ima  5940  fvssunirn  6693  mptexgf  6979  difex2  7476  oelim2  8215  omopthlem2  8277  sbthlem7  8627  unifpw  8821  fiuni  8886  rankuni  9286  rankc2  9294  rankxpu  9299  rankmapu  9301  rankxplim  9302  infxpenlem  9433  cf0  9667  fin23lem17  9754  fin23lem31  9759  smobeth  10002  nqerf  10346  dmrecnq  10384  ackbijnn  15177  divalglem2  15740  divalglem5  15742  bitsfzolem  15777  0bits  15782  bezoutlem2  15882  bezoutlem3  15883  lcmcllem  15934  lcmledvds  15937  lcmfval  15959  lcmfcllem  15963  lcmfledvds  15970  odzcllem  16123  odzdvds  16126  unbenlem  16238  4sqlem13  16287  4sqlem14  16288  4sqlem17  16291  4sqlem18  16292  vdwlem8  16318  vdwnnlem3  16327  ramcl2lem  16339  ramtcl  16340  ramtub  16342  strle1  16586  prdsval  16722  wunfunc  17163  wunnat  17220  psssdm2  17819  tsrss  17827  gicer  18410  symgsssg  18589  symgfisg  18590  odfval  18654  odlem2  18661  gexlem2  18701  torsubg  18968  dprd2da  19158  zringlpirlem2  20626  zringlpirlem3  20627  pjfval  20844  pjpm  20846  toponsspwpw  21524  eltg4i  21562  ntrss2  21659  isopn3  21668  mretopd  21694  leordtval2  21814  ptbasfi  22183  hmphtop  22380  hmpher  22386  restutop  22840  ucnprima  22885  tngtopn  23253  tgioo  23398  xrtgioo  23408  ovolicc2lem4  24115  nulmbl2  24131  iundisj  24143  dyadmax  24193  i1f1  24285  dvfval  24489  dvcnp2  24511  lhop1lem  24604  lhop2  24606  elqaalem1  24902  elqaalem3  24904  taylthlem2  24956  pserulm  25004  psercn2  25005  psercnlem2  25006  psercnlem1  25007  psercn  25008  pserdvlem1  25009  pserdvlem2  25010  pserdv  25011  pserdv2  25012  abelth  25023  dvlog  25228  efopnlem2  25234  logtayl  25237  cxpcn3lem  25322  cxpcn3  25323  resqrtcn  25324  dvatan  25507  atancn  25508  rlimcnp  25537  rlimcnp2  25538  wilthlem3  25641  ftalem4  25647  ftalem5  25648  dchrisum0lem2a  26087  cchhllem  26667  axlowdimlem6  26727  hhssabloilem  29032  choc1  29098  chub2i  29241  span0  29313  spanuni  29315  sshhococi  29317  chsup0  29319  spansnpji  29349  mayetes3i  29500  nlelshi  29831  pjimai  29947  pj3i  29979  shatomistici  30132  hatomistici  30133  atcvat4i  30168  iundisjf  30333  rinvf1o  30369  mptctf  30447  iundisjfi  30513  xrge0mulgnn0  30671  ccfldsrarelvec  31051  ccfldextdgrr  31052  xrge0iifcnv  31171  xrge0iifiso  31173  xrge0iifhom  31175  esumcvgsum  31342  coinfliprv  31735  signsply0  31816  signstcl  31830  signstf  31831  kur14lem6  32453  mthmsta  32820  bdayimaon  33192  nosupbday  33200  noetalem3  33214  noetalem4  33215  nocvxminlem  33242  nocvxmin  33243  filnetlem3  33723  filnetlem4  33724  onint1  33792  oninhaus  33793  bj-nuliotaALT  34345  imadifss  34861  poimirlem3  34889  poimirlem32  34918  dvtan  34936  itg2addnclem2  34938  ftc1anclem6  34966  heiborlem3  35085  isdrngo2  35230  elrfi  39284  mapfzcons1  39307  eldioph4b  39401  dnnumch3lem  39639  dnnumch3  39640  dgraalem  39738  dgraaub  39741  resnonrel  39945  cotrcltrcl  40063  cotrclrcl  40080  frege131d  40102  binomcxplemdvbinom  40678  binomcxplemdvsum  40680  binomcxplemnotnn0  40681  relopabVD  41228  rabexgf  41274  fzssnn0  41578  iuneqfzuzlem  41595  allbutfiinf  41687  uzublem  41697  sumnnodd  41904  lptioo2cn  41919  lptioo1cn  41920  fourierdlem31  42417  fourierdlem102  42487  fourierdlem114  42499  fouriercn  42511  elaa2lem  42512  etransclem48  42561  salexct  42611  salgencntex  42620  sge0resplit  42682  meaiuninclem  42756  caratheodorylem1  42802  hoicvr  42824  hoicvrrex  42832  hoidmvlelem3  42873  hoidmvlelem4  42874