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

Theorem sseqtri 3380
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 3373 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 200 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652    C_ wss 3320
This theorem is referenced by:  sseqtr4i  3381  eqimssi  3402  abssi  3418  ssun2  3511  difex2  4714  unixpss  4988  0ima  5222  fvssunirn  5754  oelim2  6838  omopthlem2  6899  sbthlem7  7223  unifpw  7409  fiuni  7433  rankuni  7789  rankc2  7797  rankxpu  7802  rankxplim  7803  infxpenlem  7895  cf0  8131  fin23lem17  8218  fin23lem31  8223  smobeth  8461  nqerf  8807  dmrecnq  8845  ackbijnn  12607  divalglem2  12915  divalglem5  12917  bitsfzolem  12946  0bits  12951  bezoutlem2  13039  bezoutlem3  13040  odzcllem  13178  odzdvds  13181  unbenlem  13276  4sqlem13  13325  4sqlem14  13326  4sqlem17  13329  4sqlem18  13330  vdwlem8  13356  vdwnnlem3  13365  ramcl2lem  13377  ramtcl  13378  ramtub  13380  strle1  13560  prdsval  13678  xpsc0  13785  xpsc1  13786  wunfunc  14096  wunnat  14153  psssdm2  14647  tsrss  14655  gicer  15063  odlem2  15177  gexlem2  15216  torsubg  15469  gsumzaddlem  15526  dprd2da  15600  zlpirlem2  16769  zlpirlem3  16770  pjfval  16933  pjpm  16935  eltg4i  17025  ntrss2  17121  isopn3  17130  mretopd  17156  leordtval2  17276  ptbasfi  17613  hmphtop  17810  hmpher  17816  restutop  18267  ucnprima  18312  tngtopn  18691  tgioo  18827  xrtgioo  18837  iccpnfcnv  18969  ovolicc2lem4  19416  nulmbl2  19431  iundisj  19442  dyadmax  19490  i1f1  19582  dvfval  19784  dvcnp2  19806  lhop1lem  19897  lhop2  19899  elqaalem1  20236  elqaalem3  20238  taylthlem2  20290  pserulm  20338  psercn2  20339  psercnlem2  20340  psercnlem1  20341  psercn  20342  pserdvlem1  20343  pserdvlem2  20344  pserdv  20345  pserdv2  20346  abelth  20357  dvlog  20542  efopnlem2  20548  logtayl  20551  cxpcn3lem  20631  cxpcn3  20632  resqrcn  20633  dvatan  20775  atancn  20776  rlimcnp  20804  rlimcnp2  20805  wilthlem2  20852  wilthlem3  20853  ftalem4  20858  ftalem5  20859  dchrisum0lem2a  21211  choc1  22829  chub2i  22972  span0  23044  spanuni  23046  sshhococi  23048  chsup0  23050  spansnpji  23080  mayetes3i  23232  nlelshi  23563  pjimai  23679  pj3i  23711  shatomistici  23864  hatomistici  23865  atcvat4i  23900  iundisjf  24029  rinvf1o  24042  mptctf  24112  iundisjfi  24152  xrge0mulgnn0  24210  xrge0adddir  24215  fsumrp0cl  24217  xrge0iifcnv  24319  xrge0iifiso  24321  xrge0iifhom  24323  lmlimxrge0  24334  rge0scvg  24335  lmdvg  24338  esumfsupre  24461  esumpfinvallem  24464  esumpfinval  24465  esumpfinvalf  24466  esumpcvgval  24468  esumcvg  24476  measunl  24570  coinfliprv  24740  kur14lem6  24897  nocvxminlem  25645  nocvxmin  25646  nobndlem1  25647  nobndlem2  25648  axlowdimlem6  25886  onint1  26199  oninhaus  26200  itg2addnclem2  26257  ftc1anclem6  26285  filnetlem3  26409  filnetlem4  26410  heiborlem3  26522  isdrngo2  26574  elrfi  26748  mapfzcons1  26773  eldioph4b  26872  dnnumch3lem  27121  dnnumch3  27122  dgraalem  27327  dgraaub  27330  symgsssg  27385  symgfisg  27386  rabexgf  27671  relopabVD  29013
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator