Theorem sseqtri 3637

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

Syntax hints:   = wceq 1483   ⊆ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sseqtr4i  3638  eqimssi  3659  abssi  3677  ssun2  3777  unixpss  5234  0ima  5482  idssxp  6009  fvssunirn  6217  mptexgf  6485  difex2  6969  oelim2  7675  omopthlem2  7736  sbthlem7  8076  unifpw  8269  fiuni  8334  rankuni  8726  rankc2  8734  rankxpu  8739  rankmapu  8741  rankxplim  8742  infxpenlem  8836  cf0  9073  fin23lem17  9160  fin23lem31  9165  smobeth  9408  nqerf  9752  dmrecnq  9790  ackbijnn  14560  divalglem2  15118  divalglem5  15120  bitsfzolem  15156  0bits  15161  bezoutlem2  15257  bezoutlem3  15258  lcmcllem  15309  lcmledvds  15312  lcmfval  15334  lcmfcllem  15338  lcmfledvds  15345  odzcllem  15497  odzdvds  15500  unbenlem  15612  4sqlem13  15661  4sqlem14  15662  4sqlem17  15665  4sqlem18  15666  vdwlem8  15692  vdwnnlem3  15701  ramcl2lem  15713  ramtcl  15714  ramtub  15716  strle1  15973  prdsval  16115  xpsc0  16220  xpsc1  16221  wunfunc  16559  wunnat  16616  psssdm2  17215  tsrss  17223  gicer  17718  gicerOLD  17719  symgsssg  17887  symgfisg  17888  odlem2  17958  gexlem2  17997  torsubg  18257  dprd2da  18441  zringlpirlem2  19833  zringlpirlem3  19834  pjfval  20050  pjpm  20052  toponsspwpw  20726  eltg4i  20764  ntrss2  20861  isopn3  20870  mretopd  20896  leordtval2  21016  ptbasfi  21384  hmphtop  21581  hmpher  21587  restutop  22041  ucnprima  22086  tngtopn  22454  tgioo  22599  xrtgioo  22609  ovolicc2lem4  23288  nulmbl2  23304  iundisj  23316  dyadmax  23366  i1f1  23457  dvfval  23661  dvcnp2  23683  lhop1lem  23776  lhop2  23778  elqaalem1  24074  elqaalem3  24076  taylthlem2  24128  pserulm  24176  psercn2  24177  psercnlem2  24178  psercnlem1  24179  psercn  24180  pserdvlem1  24181  pserdvlem2  24182  pserdv  24183  pserdv2  24184  abelth  24195  dvlog  24397  efopnlem2  24403  logtayl  24406  cxpcn3lem  24488  cxpcn3  24489  resqrtcn  24490  dvatan  24662  atancn  24663  rlimcnp  24692  rlimcnp2  24693  wilthlem3  24796  ftalem4  24802  ftalem5  24803  dchrisum0lem2a  25206  cchhllem  25767  axlowdimlem6  25827  hhssabloilem  28118  choc1  28186  chub2i  28329  span0  28401  spanuni  28403  sshhococi  28405  chsup0  28407  spansnpji  28437  mayetes3i  28588  nlelshi  28919  pjimai  29035  pj3i  29067  shatomistici  29220  hatomistici  29221  atcvat4i  29256  iundisjf  29402  rinvf1o  29432  mptctf  29495  iundisjfi  29555  xrge0mulgnn0  29689  xrge0iifcnv  29979  xrge0iifiso  29981  xrge0iifhom  29983  esumcvgsum  30150  coinfliprv  30544  signsply0  30628  signstcl  30642  signstf  30643  kur14lem6  31193  mthmsta  31475  bdayimaon  31843  nosupbday  31851  noetalem3  31865  noetalem4  31866  nocvxminlem  31893  nocvxmin  31894  filnetlem3  32375  filnetlem4  32376  onint1  32448  oninhaus  32449  bj-nuliotaALT  33020  imadifss  33384  poimirlem3  33412  poimirlem32  33441  dvtan  33460  itg2addnclem2  33462  ftc1anclem6  33490  heiborlem3  33612  isdrngo2  33757  elrfi  37257  mapfzcons1  37280  eldioph4b  37375  dnnumch3lem  37616  dnnumch3  37617  dgraalem  37715  dgraaub  37718  resnonrel  37898  rtrclex  37924  rtrclexi  37928  cotrcltrcl  38017  cotrclrcl  38034  frege131d  38056  binomcxplemdvbinom  38552  binomcxplemdvsum  38554  binomcxplemnotnn0  38555  relopabVD  39137  rabexgf  39183  fzssnn0  39533  iuneqfzuzlem  39550  allbutfiinf  39647  uzublem  39657  sumnnodd  39862  lptioo2cn  39877  lptioo1cn  39878  fourierdlem31  40355  fourierdlem102  40425  fourierdlem114  40437  fouriercn  40449  elaa2lem  40450  etransclem48  40499  salexct  40552  salgencntex  40561  sge0resplit  40623  meaiuninclem  40697  caratheodorylem1  40740  hoicvr  40762  hoicvrrex  40770  hoidmvlelem3  40811  hoidmvlelem4  40812