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

Theorem sseqtri 3518
Description: Substitution of equality into a subclass relationship. (Contributed by NM, 28-Jul-1995.)
Hypotheses
Ref Expression
sseqtr.1  |-  A  C_  B
sseqtr.2  |-  B  =  C
Assertion
Ref Expression
sseqtri  |-  A  C_  C

Proof of Theorem sseqtri
StepHypRef Expression
1 sseqtr.1 . 2  |-  A  C_  B
2 sseqtr.2 . . 3  |-  B  =  C
32sseq2i 3511 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 208 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1381    C_ wss 3458
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-in 3465  df-ss 3472
This theorem is referenced by:  sseqtr4i  3519  eqimssi  3540  abssi  3557  ssun2  3650  unixpss  5104  0ima  5339  fvssunirn  5875  difex2  6588  oelim2  7242  omopthlem2  7303  sbthlem7  7631  unifpw  7821  fiuni  7886  rankuni  8279  rankc2  8287  rankxpu  8292  rankmapu  8294  rankxplim  8295  infxpenlem  8389  cf0  8629  fin23lem17  8716  fin23lem31  8721  smobeth  8959  nqerf  9306  dmrecnq  9344  ackbijnn  13614  divalglem2  13925  divalglem5  13927  bitsfzolem  13956  0bits  13961  bezoutlem2  14049  bezoutlem3  14050  odzcllem  14191  odzdvds  14194  unbenlem  14298  4sqlem13  14347  4sqlem14  14348  4sqlem17  14351  4sqlem18  14352  vdwlem8  14378  vdwnnlem3  14387  ramcl2lem  14399  ramtcl  14400  ramtub  14402  strle1  14600  prdsval  14724  xpsc0  14829  xpsc1  14830  wunfunc  15137  wunnat  15194  psssdm2  15714  tsrss  15722  gicer  16193  symgsssg  16361  symgfisg  16362  odlem2  16432  gexlem2  16471  torsubg  16729  gsumzaddlemOLD  16805  dprd2da  16959  zringlpirlem2  18377  zringlpirlem3  18378  zlpirlem2  18382  zlpirlem3  18383  pjfval  18604  pjpm  18606  eltg4i  19328  ntrss2  19424  isopn3  19433  mretopd  19459  leordtval2  19579  ptbasfi  19948  hmphtop  20145  hmpher  20151  restutop  20606  ucnprima  20651  tngtopn  21030  tgioo  21167  xrtgioo  21177  ovolicc2lem4  21797  nulmbl2  21813  iundisj  21824  dyadmax  21873  i1f1  21963  dvfval  22167  dvcnp2  22189  lhop1lem  22280  lhop2  22282  elqaalem1  22580  elqaalem3  22582  taylthlem2  22634  pserulm  22682  psercn2  22683  psercnlem2  22684  psercnlem1  22685  psercn  22686  pserdvlem1  22687  pserdvlem2  22688  pserdv  22689  pserdv2  22690  abelth  22701  dvlog  22897  efopnlem2  22903  logtayl  22906  cxpcn3lem  22986  cxpcn3  22987  resqrtcn  22988  dvatan  23131  atancn  23132  rlimcnp  23160  rlimcnp2  23161  wilthlem3  23209  ftalem4  23214  ftalem5  23215  dchrisum0lem2a  23567  cchhllem  24055  axlowdimlem6  24115  choc1  26110  chub2i  26253  span0  26325  spanuni  26327  sshhococi  26329  chsup0  26331  spansnpji  26361  mayetes3i  26513  nlelshi  26844  pjimai  26960  pj3i  26992  shatomistici  27145  hatomistici  27146  atcvat4i  27181  iundisjf  27313  idssxp  27334  rinvf1o  27337  mptctf  27409  iundisjfi  27466  xrge0mulgnn0  27543  xrge0iifcnv  27781  xrge0iifiso  27783  xrge0iifhom  27785  coinfliprv  28287  signsply0  28374  signstcl  28388  signstf  28389  kur14lem6  28521  mthmsta  28804  nocvxminlem  29418  nocvxmin  29419  nobndlem1  29420  nobndlem2  29421  onint1  29882  oninhaus  29883  dvtan  30033  itg2addnclem2  30035  ftc1anclem6  30063  filnetlem3  30166  filnetlem4  30167  heiborlem3  30277  isdrngo2  30329  elrfi  30594  mapfzcons1  30617  eldioph4b  30713  dnnumch3lem  30960  dnnumch3  30961  dgraalem  31063  dgraaub  31066  lcmcllem  31171  lcmledvds  31174  rabexgf  31346  sumnnodd  31540  lptioo2cn  31555  lptioo1cn  31556  fourierdlem31  31805  fourierdlem102  31876  fourierdlem114  31888  fouriercn  31900  relopabVD  33409  bj-nuliotaALT  34299
  Copyright terms: Public domain W3C validator