Theorem sseqtri 4032

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

Syntax hints:   = wceq 1540   ⊆ wss 3951

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  sseqtrri  4033  3sstr3i  4034  eqimssi  4044  abssi  4070  ssun2  4179  unixpss  5820  0ima  6096  fvssunirnOLD  6940  mptexgf  7242  difex2  7780  oelim2  8633  omopthlem2  8698  sbthlem7  9129  unifpw  9395  fiuni  9468  dmttrcl  9761  rnttrcl  9762  ttrclexg  9763  rankuni  9903  rankc2  9911  rankxpu  9916  rankmapu  9918  rankxplim  9919  infxpenlem  10053  cf0  10291  fin23lem17  10378  fin23lem31  10383  smobeth  10626  nqerf  10970  dmrecnq  11008  ackbijnn  15864  divalglem2  16432  divalglem5  16434  bitsfzolem  16471  0bits  16476  bezoutlem2  16577  bezoutlem3  16578  lcmcllem  16633  lcmledvds  16636  lcmfval  16658  lcmfcllem  16662  lcmfledvds  16669  odzcllem  16830  odzdvds  16833  unbenlem  16946  4sqlem13  16995  4sqlem14  16996  4sqlem17  16999  4sqlem18  17000  vdwlem8  17026  vdwnnlem3  17035  ramcl2lem  17047  ramtcl  17048  ramtub  17050  strle1  17195  prdsvallem  17499  wunfunc  17946  wunnat  18004  psssdm2  18626  tsrss  18634  gicer  19295  symgsssg  19485  symgfisg  19486  odfval  19550  odlem2  19557  gexlem2  19600  torsubg  19872  dprd2da  20062  zringlpirlem2  21474  zringlpirlem3  21475  fermltlchr  21544  pjfval  21726  pjpm  21728  toponsspwpw  22928  eltg4i  22967  ntrss2  23065  isopn3  23074  mretopd  23100  leordtval2  23220  ptbasfi  23589  hmphtop  23786  hmpher  23792  restutop  24246  ucnprima  24291  tngtopn  24671  tgioo  24817  xrtgioo  24828  ovolicc2lem4  25555  nulmbl2  25571  iundisj  25583  dyadmax  25633  i1f1  25725  dvfval  25932  dvcnp2  25955  dvcnp2OLD  25956  lhop1lem  26052  lhop2  26054  elqaalem1  26361  elqaalem3  26363  taylthlem2  26416  taylthlem2OLD  26417  pserulm  26465  psercn2  26466  psercn2OLD  26467  psercnlem2  26468  psercnlem1  26469  psercn  26470  pserdvlem1  26471  pserdvlem2  26472  pserdv  26473  pserdv2  26474  abelth  26485  dvlog  26693  efopnlem2  26699  logtayl  26702  cxpcn3lem  26790  cxpcn3  26791  resqrtcn  26792  dvatan  26978  atancn  26979  rlimcnp  27008  rlimcnp2  27009  wilthlem3  27113  ftalem4  27119  ftalem5  27120  dchrisum0lem2a  27561  bdayimaon  27738  noetasuplem4  27781  noetainflem4  27785  nocvxminlem  27822  nocvxmin  27823  noeta2  27829  etasslt2  27859  scutbdaybnd2lim  27862  bday1s  27876  lrrecfr  27976  addsbdaylem  28049  negsunif  28087  zs12bday  28424  cchhllem  28901  cchhllemOLD  28902  axlowdimlem6  28962  hhssabloilem  31280  choc1  31346  chub2i  31489  span0  31561  spanuni  31563  sshhococi  31565  chsup0  31567  spansnpji  31597  mayetes3i  31748  nlelshi  32079  pjimai  32195  pj3i  32227  shatomistici  32380  hatomistici  32381  atcvat4i  32416  iundisjf  32602  rinvf1o  32640  mptctf  32729  iundisjfi  32798  xrge0mulgnn0  33020  gsumpart  33060  znfermltl  33394  ply1degltel  33615  ply1degleel  33616  ply1degltlss  33617  ccfldsrarelvec  33721  ccfldextdgrr  33722  2sqr3minply  33791  xrge0iifcnv  33932  xrge0iifiso  33934  xrge0iifhom  33936  esumcvgsum  34089  coinfliprv  34485  signsply0  34566  signstcl  34580  signstf  34581  kur14lem6  35216  mthmsta  35583  filnetlem3  36381  filnetlem4  36382  onint1  36450  oninhaus  36451  bj-nuliotaALT  37059  imadifss  37602  poimirlem3  37630  poimirlem32  37659  dvtan  37677  itg2addnclem2  37679  ftc1anclem6  37705  heiborlem3  37820  isdrngo2  37965  elrfi  42705  mapfzcons1  42728  eldioph4b  42822  dnnumch3lem  43058  dnnumch3  43059  dgraalem  43157  dgraaub  43160  resnonrel  43605  cotrcltrcl  43738  cotrclrcl  43755  frege131d  43777  binomcxplemdvbinom  44372  binomcxplemdvsum  44374  binomcxplemnotnn0  44375  relopabVD  44921  rabexgf  45029  fzssnn0  45329  iuneqfzuzlem  45345  allbutfiinf  45431  uzublem  45441  sumnnodd  45645  lptioo2cn  45660  lptioo1cn  45661  fourierdlem31  46153  fourierdlem102  46223  fourierdlem114  46235  fouriercn  46247  elaa2lem  46248  etransclem48  46297  salexct  46349  salgencntex  46358  sge0resplit  46421  meaiuninclem  46495  caratheodorylem1  46541  hoicvr  46563  hoicvrrex  46571  hoidmvlelem3  46612  hoidmvlelem4  46613  gricrel  47888  grlicrel  47966