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

Theorem sseqtri 3383
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 3376 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 208 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    C_ wss 3323
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3330  df-ss 3337
This theorem is referenced by:  sseqtr4i  3384  eqimssi  3405  abssi  3422  ssun2  3515  unixpss  4950  0ima  5180  fvssunirn  5708  difex2  6378  oelim2  7026  omopthlem2  7087  sbthlem7  7419  unifpw  7606  fiuni  7670  rankuni  8062  rankc2  8070  rankxpu  8075  rankmapu  8077  rankxplim  8078  infxpenlem  8172  cf0  8412  fin23lem17  8499  fin23lem31  8504  smobeth  8742  nqerf  9091  dmrecnq  9129  ackbijnn  13283  divalglem2  13591  divalglem5  13593  bitsfzolem  13622  0bits  13627  bezoutlem2  13715  bezoutlem3  13716  odzcllem  13856  odzdvds  13859  unbenlem  13961  4sqlem13  14010  4sqlem14  14011  4sqlem17  14014  4sqlem18  14015  vdwlem8  14041  vdwnnlem3  14050  ramcl2lem  14062  ramtcl  14063  ramtub  14065  strle1  14261  prdsval  14385  xpsc0  14490  xpsc1  14491  wunfunc  14801  wunnat  14858  psssdm2  15377  tsrss  15385  gicer  15795  symgsssg  15964  symgfisg  15965  odlem2  16033  gexlem2  16072  torsubg  16327  gsumzaddlemOLD  16401  dprd2da  16531  zringlpirlem2  17884  zringlpirlem3  17885  zlpirlem2  17889  zlpirlem3  17890  pjfval  18111  pjpm  18113  frlmip  18183  eltg4i  18545  ntrss2  18641  isopn3  18650  mretopd  18676  leordtval2  18796  ptbasfi  19134  hmphtop  19331  hmpher  19337  restutop  19792  ucnprima  19837  tngtopn  20216  tgioo  20353  xrtgioo  20363  iccpnfcnv  20496  rrxip  20874  ovolicc2lem4  20983  nulmbl2  20998  iundisj  21009  dyadmax  21058  i1f1  21148  dvfval  21352  dvcnp2  21374  lhop1lem  21465  lhop2  21467  elqaalem1  21765  elqaalem3  21767  taylthlem2  21819  pserulm  21867  psercn2  21868  psercnlem2  21869  psercnlem1  21870  psercn  21871  pserdvlem1  21872  pserdvlem2  21873  pserdv  21874  pserdv2  21875  abelth  21886  dvlog  22076  efopnlem2  22082  logtayl  22085  cxpcn3lem  22165  cxpcn3  22166  resqrcn  22167  dvatan  22310  atancn  22311  rlimcnp  22339  rlimcnp2  22340  wilthlem3  22388  ftalem4  22393  ftalem5  22394  dchrisum0lem2a  22746  cchhllem  23101  axlowdimlem6  23161  choc1  24698  chub2i  24841  span0  24913  spanuni  24915  sshhococi  24917  chsup0  24919  spansnpji  24949  mayetes3i  25101  nlelshi  25432  pjimai  25548  pj3i  25580  shatomistici  25733  hatomistici  25734  atcvat4i  25769  iundisjf  25899  rinvf1o  25917  mptctf  25989  iundisjfi  26048  xrge0mulgnn0  26118  gsumle  26214  xrge0iifcnv  26332  xrge0iifiso  26334  xrge0iifhom  26336  esumfsupre  26489  esumpfinvallem  26492  esumpcvgval  26496  esumcvg  26504  measunl  26599  coinfliprv  26834  signsply0  26921  signstcl  26935  signstf  26936  kur14lem6  27068  nocvxminlem  27800  nocvxmin  27801  nobndlem1  27802  nobndlem2  27803  onint1  28265  oninhaus  28266  dvtan  28413  itg2addnclem2  28415  ftc1anclem6  28443  filnetlem3  28572  filnetlem4  28573  heiborlem3  28683  isdrngo2  28735  elrfi  29001  mapfzcons1  29024  eldioph4b  29121  dnnumch3lem  29370  dnnumch3  29371  dgraalem  29473  dgraaub  29476  rabexgf  29717  relopabVD  31566
  Copyright terms: Public domain W3C validator