Theorem sseqtri 4014

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

Syntax hints:   = wceq 1534   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2698

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1537  df-ex 1775  df-sb 2061  df-clab 2705  df-cleq 2719  df-clel 2805  df-v 3471  df-in 3951  df-ss 3961

This theorem is referenced by:  sseqtrri  4015  eqimssi  4038  abssi  4063  ssun2  4169  unixpss  5806  0ima  6075  fvssunirnOLD  6925  mptexgf  7228  difex2  7756  oelim2  8609  omopthlem2  8674  sbthlem7  9105  unifpw  9371  fiuni  9443  dmttrcl  9736  rnttrcl  9737  ttrclexg  9738  rankuni  9878  rankc2  9886  rankxpu  9891  rankmapu  9893  rankxplim  9894  infxpenlem  10028  cf0  10266  fin23lem17  10353  fin23lem31  10358  smobeth  10601  nqerf  10945  dmrecnq  10983  ackbijnn  15798  divalglem2  16363  divalglem5  16365  bitsfzolem  16400  0bits  16405  bezoutlem2  16507  bezoutlem3  16508  lcmcllem  16558  lcmledvds  16561  lcmfval  16583  lcmfcllem  16587  lcmfledvds  16594  odzcllem  16752  odzdvds  16755  unbenlem  16868  4sqlem13  16917  4sqlem14  16918  4sqlem17  16921  4sqlem18  16922  vdwlem8  16948  vdwnnlem3  16957  ramcl2lem  16969  ramtcl  16970  ramtub  16972  strle1  17118  prdsvallem  17427  wunfunc  17878  wunfuncOLD  17879  wunnat  17937  wunnatOLD  17938  psssdm2  18564  tsrss  18572  gicer  19222  symgsssg  19413  symgfisg  19414  odfval  19478  odlem2  19485  gexlem2  19528  torsubg  19800  dprd2da  19990  zringlpirlem2  21376  zringlpirlem3  21377  fermltlchr  21446  pjfval  21627  pjpm  21629  toponsspwpw  22811  eltg4i  22850  ntrss2  22948  isopn3  22957  mretopd  22983  leordtval2  23103  ptbasfi  23472  hmphtop  23669  hmpher  23675  restutop  24129  ucnprima  24174  tngtopn  24554  tgioo  24699  xrtgioo  24709  ovolicc2lem4  25436  nulmbl2  25452  iundisj  25464  dyadmax  25514  i1f1  25606  dvfval  25813  dvcnp2  25836  dvcnp2OLD  25837  lhop1lem  25933  lhop2  25935  elqaalem1  26241  elqaalem3  26243  taylthlem2  26296  taylthlem2OLD  26297  pserulm  26345  psercn2  26346  psercn2OLD  26347  psercnlem2  26348  psercnlem1  26349  psercn  26350  pserdvlem1  26351  pserdvlem2  26352  pserdv  26353  pserdv2  26354  abelth  26365  dvlog  26572  efopnlem2  26578  logtayl  26581  cxpcn3lem  26669  cxpcn3  26670  resqrtcn  26671  dvatan  26854  atancn  26855  rlimcnp  26884  rlimcnp2  26885  wilthlem3  26989  ftalem4  26995  ftalem5  26996  dchrisum0lem2a  27437  bdayimaon  27613  noetasuplem4  27656  noetainflem4  27660  nocvxminlem  27697  nocvxmin  27698  noeta2  27704  etasslt2  27734  scutbdaybnd2lim  27737  bday1s  27751  lrrecfr  27847  negsunif  27954  cchhllem  28684  cchhllemOLD  28685  axlowdimlem6  28745  hhssabloilem  31058  choc1  31124  chub2i  31267  span0  31339  spanuni  31341  sshhococi  31343  chsup0  31345  spansnpji  31375  mayetes3i  31526  nlelshi  31857  pjimai  31973  pj3i  32005  shatomistici  32158  hatomistici  32159  atcvat4i  32194  iundisjf  32364  rinvf1o  32398  mptctf  32483  iundisjfi  32548  xrge0mulgnn0  32727  gsumpart  32747  znfermltl  33018  ply1degltel  33197  ply1degleel  33198  ply1degltlss  33199  ccfldsrarelvec  33291  ccfldextdgrr  33292  xrge0iifcnv  33470  xrge0iifiso  33472  xrge0iifhom  33474  esumcvgsum  33643  coinfliprv  34038  signsply0  34119  signstcl  34133  signstf  34134  kur14lem6  34757  mthmsta  35124  filnetlem3  35800  filnetlem4  35801  onint1  35869  oninhaus  35870  bj-nuliotaALT  36473  imadifss  37003  poimirlem3  37031  poimirlem32  37060  dvtan  37078  itg2addnclem2  37080  ftc1anclem6  37106  heiborlem3  37221  isdrngo2  37366  elrfi  42036  mapfzcons1  42059  eldioph4b  42153  dnnumch3lem  42392  dnnumch3  42393  dgraalem  42491  dgraaub  42494  resnonrel  42945  cotrcltrcl  43078  cotrclrcl  43095  frege131d  43117  binomcxplemdvbinom  43713  binomcxplemdvsum  43715  binomcxplemnotnn0  43716  relopabVD  44263  rabexgf  44309  fzssnn0  44622  iuneqfzuzlem  44639  allbutfiinf  44725  uzublem  44735  sumnnodd  44941  lptioo2cn  44956  lptioo1cn  44957  fourierdlem31  45449  fourierdlem102  45519  fourierdlem114  45531  fouriercn  45543  elaa2lem  45544  etransclem48  45593  salexct  45645  salgencntex  45654  sge0resplit  45717  meaiuninclem  45791  caratheodorylem1  45837  hoicvr  45859  hoicvrrex  45867  hoidmvlelem3  45908  hoidmvlelem4  45909  gricrel  47108