Theorem sseqtri 3979

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

This proof depends on syntax axioms:   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  sseqtrri  3980  3sstr3i  3981  eqimssi  3991  abssi  4016  ssun2  4125  unixpss  5788  0ima  6072  imadifssran  6195  mptexgf  7220  difex2  7763  oelim2  8588  omopthlem2  8653  sbthlem7  9096  unifpw  9328  fiuni  9404  dmttrcl  9706  rnttrcl  9707  ttrclexg  9708  rankuni  9860  rankc2  9869  rankxpu  9874  rankmapu  9876  rankxplim  9877  infxpenlem  10073  cf0  10309  fin23lem17  10397  fin23lem31  10402  smobeth  10652  nqerf  10996  dmrecnq  11034  ackbijnn  15977  divalglem2  16545  divalglem5  16547  bitsfzolem  16584  0bits  16589  bezoutlem2  16693  bezoutlem3  16694  lcmcllem  16751  lcmledvds  16754  lcmfval  16776  lcmfcllem  16780  lcmfledvds  16787  odzcllem  16950  odzdvds  16953  unbenlem  17066  4sqlem13  17115  4sqlem14  17116  4sqlem17  17119  4sqlem18  17120  vdwlem8  17146  vdwnnlem3  17155  ramcl2lem  17167  ramtcl  17168  ramtub  17170  strle1  17316  prdsvallem  17605  wunfunc  18056  wunnat  18114  psssdm2  18735  tsrss  18743  gicer  19471  symgsssg  19661  symgfisg  19662  odfval  19726  odlem2  19733  gexlem2  19776  torsubg  20048  dprd2da  20238  ricrel  20724  zringlpirlem2  21749  zringlpirlem3  21750  fermltlchr  21815  pjfval  21992  pjpm  21994  toponsspwpw  23220  eltg4i  23258  ntrss2  23355  isopn3  23364  mretopd  23390  leordtval2  23510  ptbasfi  23880  hmphtop  24077  hmpher  24083  restutop  24536  ucnprima  24580  tngtopn  24949  tgioo  25095  xrtgioo  25106  ovolicc2lem4  25821  nulmbl2  25837  iundisj  25849  dyadmax  25899  i1f1  25991  dvfval  26197  dvcnp2  26220  lhop1lem  26313  lhop2  26315  elqaalem1  26624  elqaalem3  26626  taylthlem2  26683  pserulm  26731  psercn2  26732  psercnlem2  26733  psercnlem1  26734  psercn  26735  pserdvlem1  26736  pserdvlem2  26737  pserdv  26738  pserdv2  26739  abelth  26750  dvlog  26961  efopnlem2  26967  logtayl  26970  cxpcn3lem  27057  cxpcn3  27058  resqrtcn  27059  dvatan  27245  atancn  27246  rlimcnp  27275  rlimcnp2  27276  wilthlem3  27379  ftalem4  27385  ftalem5  27386  dchrisum0lem2a  27826  bdayimaon  28032  noetasuplem4  28075  noetainflem4  28079  nobdaymin  28121  nocvxminlem  28122  noeta2  28129  etaslts2  28162  cutbdaybnd2lim  28165  bday1  28182  lrrecfr  28311  addbdaylem  28385  negsunif  28423  oniso  28639  bdayons  28644  cchhllem  29446  axlowdimlem6  29507  hhssabloilem  31845  choc1  31911  chub2i  32054  span0  32126  spanuni  32128  sshhococi  32130  chsup0  32132  spansnpji  32162  mayetes3i  32313  nlelshi  32644  pjimai  32760  pj3i  32792  shatomistici  32945  hatomistici  32946  atcvat4i  32981  iundisjf  33165  rinvf1o  33206  mptctf  33290  iundisjfi  33370  xrge0mulgnn0  33558  gsumpart  33606  znfermltl  33904  ply1degltel  34108  ply1degleel  34109  ply1degltlss  34110  0mplrim  34128  ccfldsrarelvec  34285  ccfldextdgrr  34286  2sqr3minply  34394  xrge0iifcnv  34547  xrge0iifiso  34549  xrge0iifhom  34551  esumcvgsum  34702  coinfliprv  35098  signsply0  35163  signstcl  35177  signstf  35178  kur14lem6  35945  mthmsta  36312  filnetlem3  37138  filnetlem4  37139  onint1  37207  oninhaus  37208  bj-nuliotaALT  37941  imadifss  38491  poimirlem3  38509  poimirlem32  38538  dvtan  38556  itg2addnclem2  38558  ftc1anclem6  38584  heiborlem3  38715  isdrngo2  38860  elrfi  43658  mapfzcons1  43681  eldioph4b  43771  dnnumch3lem  44006  dnnumch3  44007  dgraalem  44105  dgraaub  44108  resnonrel  44551  cotrcltrcl  44684  cotrclrcl  44701  frege131d  44723  binomcxplemdvbinom  45296  binomcxplemdvsum  45298  binomcxplemnotnn0  45299  relopabVD  45842  rabexgf  45984  fzssnn0  46275  iuneqfzuzlem  46290  allbutfiinf  46374  uzublem  46384  sumnnodd  46586  lptioo2cn  46599  lptioo1cn  46600  fourierdlem31  47092  fourierdlem102  47162  fourierdlem114  47174  fouriercn  47186  elaa2lem  47187  etransclem48  47236  salexct  47288  salgencntex  47297  sge0resplit  47360  meaiuninclem  47434  caratheodorylem1  47480  hoicvr  47502  hoicvrrex  47510  hoidmvlelem3  47551  hoidmvlelem4  47552  gricrel  48961  grlicrel  49048