Theorem sseqtri 3986

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

Syntax hints:   = wceq 1540   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  sseqtrri  3987  3sstr3i  3988  eqimssi  3998  abssi  4023  ssun2  4132  unixpss  5757  0ima  6033  fvssunirnOLD  6858  mptexgf  7162  difex2  7700  oelim2  8520  omopthlem2  8585  sbthlem7  9017  unifpw  9264  fiuni  9337  dmttrcl  9636  rnttrcl  9637  ttrclexg  9638  rankuni  9778  rankc2  9786  rankxpu  9791  rankmapu  9793  rankxplim  9794  infxpenlem  9926  cf0  10164  fin23lem17  10251  fin23lem31  10256  smobeth  10499  nqerf  10843  dmrecnq  10881  ackbijnn  15753  divalglem2  16324  divalglem5  16326  bitsfzolem  16363  0bits  16368  bezoutlem2  16469  bezoutlem3  16470  lcmcllem  16525  lcmledvds  16528  lcmfval  16550  lcmfcllem  16554  lcmfledvds  16561  odzcllem  16722  odzdvds  16725  unbenlem  16838  4sqlem13  16887  4sqlem14  16888  4sqlem17  16891  4sqlem18  16892  vdwlem8  16918  vdwnnlem3  16927  ramcl2lem  16939  ramtcl  16940  ramtub  16942  strle1  17087  prdsvallem  17376  wunfunc  17826  wunnat  17884  psssdm2  18505  tsrss  18513  gicer  19174  symgsssg  19364  symgfisg  19365  odfval  19429  odlem2  19436  gexlem2  19479  torsubg  19751  dprd2da  19941  zringlpirlem2  21388  zringlpirlem3  21389  fermltlchr  21454  pjfval  21631  pjpm  21633  toponsspwpw  22825  eltg4i  22863  ntrss2  22960  isopn3  22969  mretopd  22995  leordtval2  23115  ptbasfi  23484  hmphtop  23681  hmpher  23687  restutop  24141  ucnprima  24185  tngtopn  24554  tgioo  24700  xrtgioo  24711  ovolicc2lem4  25437  nulmbl2  25453  iundisj  25465  dyadmax  25515  i1f1  25607  dvfval  25814  dvcnp2  25837  dvcnp2OLD  25838  lhop1lem  25934  lhop2  25936  elqaalem1  26243  elqaalem3  26245  taylthlem2  26298  taylthlem2OLD  26299  pserulm  26347  psercn2  26348  psercn2OLD  26349  psercnlem2  26350  psercnlem1  26351  psercn  26352  pserdvlem1  26353  pserdvlem2  26354  pserdv  26355  pserdv2  26356  abelth  26367  dvlog  26576  efopnlem2  26582  logtayl  26585  cxpcn3lem  26673  cxpcn3  26674  resqrtcn  26675  dvatan  26861  atancn  26862  rlimcnp  26891  rlimcnp2  26892  wilthlem3  26996  ftalem4  27002  ftalem5  27003  dchrisum0lem2a  27444  bdayimaon  27621  noetasuplem4  27664  noetainflem4  27668  nobdaymin  27705  nocvxminlem  27706  noeta2  27713  etasslt2  27743  scutbdaybnd2lim  27746  bday1s  27763  lrrecfr  27873  addsbdaylem  27946  negsunif  27984  onsiso  28192  bdayon  28196  zs12bday  28379  cchhllem  28850  axlowdimlem6  28910  hhssabloilem  31223  choc1  31289  chub2i  31432  span0  31504  spanuni  31506  sshhococi  31508  chsup0  31510  spansnpji  31540  mayetes3i  31691  nlelshi  32022  pjimai  32138  pj3i  32170  shatomistici  32323  hatomistici  32324  atcvat4i  32359  iundisjf  32551  rinvf1o  32587  mptctf  32674  iundisjfi  32752  xrge0mulgnn0  32982  gsumpart  33023  znfermltl  33313  ply1degltel  33536  ply1degleel  33537  ply1degltlss  33538  ccfldsrarelvec  33642  ccfldextdgrr  33643  2sqr3minply  33746  xrge0iifcnv  33899  xrge0iifiso  33901  xrge0iifhom  33903  esumcvgsum  34054  coinfliprv  34450  signsply0  34518  signstcl  34532  signstf  34533  kur14lem6  35183  mthmsta  35550  filnetlem3  36353  filnetlem4  36354  onint1  36422  oninhaus  36423  bj-nuliotaALT  37031  imadifss  37574  poimirlem3  37602  poimirlem32  37631  dvtan  37649  itg2addnclem2  37651  ftc1anclem6  37677  heiborlem3  37792  isdrngo2  37937  elrfi  42667  mapfzcons1  42690  eldioph4b  42784  dnnumch3lem  43019  dnnumch3  43020  dgraalem  43118  dgraaub  43121  resnonrel  43565  cotrcltrcl  43698  cotrclrcl  43715  frege131d  43737  binomcxplemdvbinom  44326  binomcxplemdvsum  44328  binomcxplemnotnn0  44329  relopabVD  44874  rabexgf  45002  fzssnn0  45298  iuneqfzuzlem  45314  allbutfiinf  45400  uzublem  45410  sumnnodd  45612  lptioo2cn  45627  lptioo1cn  45628  fourierdlem31  46120  fourierdlem102  46190  fourierdlem114  46202  fouriercn  46214  elaa2lem  46215  etransclem48  46264  salexct  46316  salgencntex  46325  sge0resplit  46388  meaiuninclem  46462  caratheodorylem1  46508  hoicvr  46530  hoicvrrex  46538  hoidmvlelem3  46579  hoidmvlelem4  46580  gricrel  47903  grlicrel  47982