MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseqtri Structured version   Visualization version   GIF version

Theorem sseqtri 3599
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
StepHypRef Expression
1 sseqtr.1 . 2 𝐴𝐵
2 sseqtr.2 . . 3 𝐵 = 𝐶
32sseq2i 3592 . 2 (𝐴𝐵𝐴𝐶)
41, 3mpbi 218 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  sseqtr4i  3600  eqimssi  3621  abssi  3639  ssun2  3738  unixpss  5146  0ima  5388  fvssunirn  6112  difex2  6840  oelim2  7539  omopthlem2  7600  sbthlem7  7938  unifpw  8129  fiuni  8194  rankuni  8586  rankc2  8594  rankxpu  8599  rankmapu  8601  rankxplim  8602  infxpenlem  8696  cf0  8933  fin23lem17  9020  fin23lem31  9025  smobeth  9264  nqerf  9608  dmrecnq  9646  ackbijnn  14345  divalglem2  14902  divalglem5  14904  bitsfzolem  14940  0bits  14945  bezoutlem2  15041  bezoutlem3  15042  lcmcllem  15093  lcmledvds  15096  lcmfval  15118  lcmfcllem  15122  lcmfledvds  15129  odzcllem  15281  odzdvds  15284  unbenlem  15396  4sqlem13  15445  4sqlem14  15446  4sqlem17  15449  4sqlem18  15450  vdwlem8  15476  vdwnnlem3  15485  ramcl2lem  15497  ramtcl  15498  ramtub  15500  strle1  15746  prdsval  15884  xpsc0  15989  xpsc1  15990  wunfunc  16328  wunnat  16385  psssdm2  16984  tsrss  16992  gicer  17487  gicerOLD  17488  symgsssg  17656  symgfisg  17657  odlem2  17727  gexlem2  17766  torsubg  18026  dprd2da  18210  zringlpirlem2  19598  zringlpirlem3  19599  pjfval  19811  pjpm  19813  eltg4i  20517  ntrss2  20613  isopn3  20622  mretopd  20648  leordtval2  20768  ptbasfi  21136  hmphtop  21333  hmpher  21339  restutop  21793  ucnprima  21838  tngtopn  22202  tgioo  22339  xrtgioo  22349  ovolicc2lem4  23012  nulmbl2  23028  iundisj  23040  dyadmax  23089  i1f1  23180  dvfval  23384  dvcnp2  23406  lhop1lem  23497  lhop2  23499  elqaalem1  23795  elqaalem3  23797  taylthlem2  23849  pserulm  23897  psercn2  23898  psercnlem2  23899  psercnlem1  23900  psercn  23901  pserdvlem1  23902  pserdvlem2  23903  pserdv  23904  pserdv2  23905  abelth  23916  dvlog  24114  efopnlem2  24120  logtayl  24123  cxpcn3lem  24205  cxpcn3  24206  resqrtcn  24207  dvatan  24379  atancn  24380  rlimcnp  24409  rlimcnp2  24410  wilthlem3  24513  ftalem4  24519  ftalem5  24520  dchrisum0lem2a  24923  cchhllem  25485  axlowdimlem6  25545  hhssabloilem  27308  choc1  27376  chub2i  27519  span0  27591  spanuni  27593  sshhococi  27595  chsup0  27597  spansnpji  27627  mayetes3i  27778  nlelshi  28109  pjimai  28225  pj3i  28257  shatomistici  28410  hatomistici  28411  atcvat4i  28446  iundisjf  28590  mptexgf  28615  idssxp  28617  rinvf1o  28620  mptctf  28689  iundisjfi  28748  xrge0mulgnn0  28826  xrge0iifcnv  29113  xrge0iifiso  29115  xrge0iifhom  29117  esumcvgsum  29283  coinfliprv  29677  signsply0  29760  signstcl  29774  signstf  29775  kur14lem6  30253  mthmsta  30535  nocvxminlem  30895  nocvxmin  30896  nobndlem1  30897  nobndlem2  30898  filnetlem3  31351  filnetlem4  31352  onint1  31424  oninhaus  31425  bj-nuliotaALT  32007  bj-sspwpweq  32036  bj-toponss  32037  imadifss  32350  poimirlem3  32378  poimirlem32  32407  dvtan  32426  itg2addnclem2  32428  ftc1anclem6  32456  heiborlem3  32578  isdrngo2  32723  elrfi  36071  mapfzcons1  36094  eldioph4b  36189  dnnumch3lem  36430  dnnumch3  36431  dgraalem  36530  dgraaub  36533  resnonrel  36713  rtrclex  36739  rtrclexi  36743  cotrcltrcl  36832  cotrclrcl  36849  frege131d  36871  binomcxplemdvbinom  37370  binomcxplemdvsum  37372  binomcxplemnotnn0  37373  relopabVD  37955  rabexgf  38002  fzssnn0  38271  iuneqfzuzlem  38288  sumnnodd  38494  lptioo2cn  38509  lptioo1cn  38510  fourierdlem31  38828  fourierdlem102  38898  fourierdlem114  38910  fouriercn  38922  elaa2lem  38923  etransclem48  38972  salexct  39025  salgencntex  39034  sge0resplit  39096  meaiuninclem  39170  caratheodorylem1  39213  hoicvr  39235  hoicvrrex  39243  hoidmvlelem3  39284  hoidmvlelem4  39285
  Copyright terms: Public domain W3C validator