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

Theorem sseqtri 3778
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 3771 . 2 (𝐴𝐵𝐴𝐶)
41, 3mpbi 220 1 𝐴𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1632  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729
This theorem is referenced by:  sseqtr4i  3779  eqimssi  3800  abssi  3818  ssun2  3920  unixpss  5390  0ima  5640  idssxp  6170  fvssunirn  6378  mptexgf  6649  difex2  7134  oelim2  7844  omopthlem2  7905  sbthlem7  8241  unifpw  8434  fiuni  8499  rankuni  8899  rankc2  8907  rankxpu  8912  rankmapu  8914  rankxplim  8915  infxpenlem  9026  cf0  9265  fin23lem17  9352  fin23lem31  9357  smobeth  9600  nqerf  9944  dmrecnq  9982  ackbijnn  14759  divalglem2  15320  divalglem5  15322  bitsfzolem  15358  0bits  15363  bezoutlem2  15459  bezoutlem3  15460  lcmcllem  15511  lcmledvds  15514  lcmfval  15536  lcmfcllem  15540  lcmfledvds  15547  odzcllem  15699  odzdvds  15702  unbenlem  15814  4sqlem13  15863  4sqlem14  15864  4sqlem17  15867  4sqlem18  15868  vdwlem8  15894  vdwnnlem3  15903  ramcl2lem  15915  ramtcl  15916  ramtub  15918  strle1  16175  prdsval  16317  xpsc0  16422  xpsc1  16423  wunfunc  16760  wunnat  16817  psssdm2  17416  tsrss  17424  gicer  17919  symgsssg  18087  symgfisg  18088  odlem2  18158  gexlem2  18197  torsubg  18457  dprd2da  18641  zringlpirlem2  20035  zringlpirlem3  20036  pjfval  20252  pjpm  20254  toponsspwpw  20928  eltg4i  20966  ntrss2  21063  isopn3  21072  mretopd  21098  leordtval2  21218  ptbasfi  21586  hmphtop  21783  hmpher  21789  restutop  22242  ucnprima  22287  tngtopn  22655  tgioo  22800  xrtgioo  22810  ovolicc2lem4  23488  nulmbl2  23504  iundisj  23516  dyadmax  23566  i1f1  23656  dvfval  23860  dvcnp2  23882  lhop1lem  23975  lhop2  23977  elqaalem1  24273  elqaalem3  24275  taylthlem2  24327  pserulm  24375  psercn2  24376  psercnlem2  24377  psercnlem1  24378  psercn  24379  pserdvlem1  24380  pserdvlem2  24381  pserdv  24382  pserdv2  24383  abelth  24394  dvlog  24596  efopnlem2  24602  logtayl  24605  cxpcn3lem  24687  cxpcn3  24688  resqrtcn  24689  dvatan  24861  atancn  24862  rlimcnp  24891  rlimcnp2  24892  wilthlem3  24995  ftalem4  25001  ftalem5  25002  dchrisum0lem2a  25405  cchhllem  25966  axlowdimlem6  26026  hhssabloilem  28427  choc1  28495  chub2i  28638  span0  28710  spanuni  28712  sshhococi  28714  chsup0  28716  spansnpji  28746  mayetes3i  28897  nlelshi  29228  pjimai  29344  pj3i  29376  shatomistici  29529  hatomistici  29530  atcvat4i  29565  iundisjf  29709  rinvf1o  29741  mptctf  29804  iundisjfi  29864  xrge0mulgnn0  29998  xrge0iifcnv  30288  xrge0iifiso  30290  xrge0iifhom  30292  esumcvgsum  30459  coinfliprv  30853  signsply0  30937  signstcl  30951  signstf  30952  kur14lem6  31500  mthmsta  31782  bdayimaon  32149  nosupbday  32157  noetalem3  32171  noetalem4  32172  nocvxminlem  32199  nocvxmin  32200  filnetlem3  32681  filnetlem4  32682  onint1  32754  oninhaus  32755  bj-nuliotaALT  33326  imadifss  33697  poimirlem3  33725  poimirlem32  33754  dvtan  33773  itg2addnclem2  33775  ftc1anclem6  33803  heiborlem3  33925  isdrngo2  34070  elrfi  37759  mapfzcons1  37782  eldioph4b  37877  dnnumch3lem  38118  dnnumch3  38119  dgraalem  38217  dgraaub  38220  resnonrel  38400  rtrclex  38426  rtrclexi  38430  cotrcltrcl  38519  cotrclrcl  38536  frege131d  38558  binomcxplemdvbinom  39054  binomcxplemdvsum  39056  binomcxplemnotnn0  39057  relopabVD  39636  rabexgf  39682  fzssnn0  40031  iuneqfzuzlem  40048  allbutfiinf  40145  uzublem  40155  sumnnodd  40365  lptioo2cn  40380  lptioo1cn  40381  fourierdlem31  40858  fourierdlem102  40928  fourierdlem114  40940  fouriercn  40952  elaa2lem  40953  etransclem48  41002  salexct  41055  salgencntex  41064  sge0resplit  41126  meaiuninclem  41200  caratheodorylem1  41246  hoicvr  41268  hoicvrrex  41276  hoidmvlelem3  41317  hoidmvlelem4  41318
  Copyright terms: Public domain W3C validator