Theorem sseqtri 3962

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

Syntax hints:   = wceq 1539   ⊆ wss 3892

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909

This theorem is referenced by:  sseqtrri  3963  eqimssi  3984  abssi  4009  ssun2  4113  unixpss  5732  0ima  5996  fvssunirn  6835  mptexgf  7130  difex2  7642  oelim2  8457  omopthlem2  8521  sbthlem7  8914  unifpw  9166  fiuni  9231  dmttrcl  9523  rnttrcl  9524  ttrclexg  9525  rankuni  9665  rankc2  9673  rankxpu  9678  rankmapu  9680  rankxplim  9681  infxpenlem  9815  cf0  10053  fin23lem17  10140  fin23lem31  10145  smobeth  10388  nqerf  10732  dmrecnq  10770  ackbijnn  15585  divalglem2  16149  divalglem5  16151  bitsfzolem  16186  0bits  16191  bezoutlem2  16293  bezoutlem3  16294  lcmcllem  16346  lcmledvds  16349  lcmfval  16371  lcmfcllem  16375  lcmfledvds  16382  odzcllem  16538  odzdvds  16541  unbenlem  16654  4sqlem13  16703  4sqlem14  16704  4sqlem17  16707  4sqlem18  16708  vdwlem8  16734  vdwnnlem3  16743  ramcl2lem  16755  ramtcl  16756  ramtub  16758  strle1  16904  prdsvallem  17210  wunfunc  17659  wunfuncOLD  17660  wunnat  17717  wunnatOLD  17718  psssdm2  18344  tsrss  18352  gicer  18937  symgsssg  19120  symgfisg  19121  odfval  19185  odlem2  19192  gexlem2  19232  torsubg  19500  dprd2da  19690  zringlpirlem2  20730  zringlpirlem3  20731  pjfval  20958  pjpm  20960  toponsspwpw  22116  eltg4i  22155  ntrss2  22253  isopn3  22262  mretopd  22288  leordtval2  22408  ptbasfi  22777  hmphtop  22974  hmpher  22980  restutop  23434  ucnprima  23479  tngtopn  23859  tgioo  24004  xrtgioo  24014  ovolicc2lem4  24729  nulmbl2  24745  iundisj  24757  dyadmax  24807  i1f1  24899  dvfval  25106  dvcnp2  25129  lhop1lem  25222  lhop2  25224  elqaalem1  25524  elqaalem3  25526  taylthlem2  25578  pserulm  25626  psercn2  25627  psercnlem2  25628  psercnlem1  25629  psercn  25630  pserdvlem1  25631  pserdvlem2  25632  pserdv  25633  pserdv2  25634  abelth  25645  dvlog  25851  efopnlem2  25857  logtayl  25860  cxpcn3lem  25945  cxpcn3  25946  resqrtcn  25947  dvatan  26130  atancn  26131  rlimcnp  26160  rlimcnp2  26161  wilthlem3  26264  ftalem4  26270  ftalem5  26271  dchrisum0lem2a  26710  cchhllem  27299  cchhllemOLD  27300  axlowdimlem6  27360  hhssabloilem  29668  choc1  29734  chub2i  29877  span0  29949  spanuni  29951  sshhococi  29953  chsup0  29955  spansnpji  29985  mayetes3i  30136  nlelshi  30467  pjimai  30583  pj3i  30615  shatomistici  30768  hatomistici  30769  atcvat4i  30804  iundisjf  30973  rinvf1o  31010  mptctf  31097  iundisjfi  31162  xrge0mulgnn0  31343  gsumpart  31360  znfermltl  31607  ccfldsrarelvec  31786  ccfldextdgrr  31787  xrge0iifcnv  31928  xrge0iifiso  31930  xrge0iifhom  31932  esumcvgsum  32101  coinfliprv  32494  signsply0  32575  signstcl  32589  signstf  32590  kur14lem6  33218  mthmsta  33585  bdayimaon  33941  noetasuplem4  33984  noetainflem4  33988  nocvxminlem  34017  nocvxmin  34018  noeta2  34024  etasslt2  34053  scutbdaybnd2lim  34056  bday1s  34070  lrrecfr  34145  filnetlem3  34614  filnetlem4  34615  onint1  34683  oninhaus  34684  bj-nuliotaALT  35273  imadifss  35796  poimirlem3  35824  poimirlem32  35853  dvtan  35871  itg2addnclem2  35873  ftc1anclem6  35899  heiborlem3  36015  isdrngo2  36160  elrfi  40553  mapfzcons1  40576  eldioph4b  40670  dnnumch3lem  40909  dnnumch3  40910  dgraalem  41008  dgraaub  41011  resnonrel  41238  cotrcltrcl  41371  cotrclrcl  41388  frege131d  41410  binomcxplemdvbinom  42009  binomcxplemdvsum  42011  binomcxplemnotnn0  42012  relopabVD  42559  rabexgf  42605  fzssnn0  42904  iuneqfzuzlem  42921  allbutfiinf  43008  uzublem  43018  sumnnodd  43220  lptioo2cn  43235  lptioo1cn  43236  fourierdlem31  43728  fourierdlem102  43798  fourierdlem114  43810  fouriercn  43822  elaa2lem  43823  etransclem48  43872  salexct  43922  salgencntex  43931  sge0resplit  43994  meaiuninclem  44068  caratheodorylem1  44114  hoicvr  44136  hoicvrrex  44144  hoidmvlelem3  44185  hoidmvlelem4  44186