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

Theorem sseqtri 3529
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 3522 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 208 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1374    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-in 3476  df-ss 3483
This theorem is referenced by:  sseqtr4i  3530  eqimssi  3551  abssi  3568  ssun2  3661  unixpss  5109  0ima  5344  fvssunirn  5880  difex2  6578  oelim2  7234  omopthlem2  7295  sbthlem7  7623  unifpw  7812  fiuni  7877  rankuni  8270  rankc2  8278  rankxpu  8283  rankmapu  8285  rankxplim  8286  infxpenlem  8380  cf0  8620  fin23lem17  8707  fin23lem31  8712  smobeth  8950  nqerf  9297  dmrecnq  9335  ackbijnn  13592  divalglem2  13901  divalglem5  13903  bitsfzolem  13932  0bits  13937  bezoutlem2  14025  bezoutlem3  14026  odzcllem  14167  odzdvds  14170  unbenlem  14274  4sqlem13  14323  4sqlem14  14324  4sqlem17  14327  4sqlem18  14328  vdwlem8  14354  vdwnnlem3  14363  ramcl2lem  14375  ramtcl  14376  ramtub  14378  strle1  14575  prdsval  14699  xpsc0  14804  xpsc1  14805  wunfunc  15115  wunnat  15172  psssdm2  15691  tsrss  15699  gicer  16112  symgsssg  16281  symgfisg  16282  odlem2  16352  gexlem2  16391  torsubg  16646  gsumzaddlemOLD  16720  dprd2da  16874  zringlpirlem2  18270  zringlpirlem3  18271  zlpirlem2  18275  zlpirlem3  18276  pjfval  18497  pjpm  18499  frlmip  18569  eltg4i  19221  ntrss2  19317  isopn3  19326  mretopd  19352  leordtval2  19472  ptbasfi  19810  hmphtop  20007  hmpher  20013  restutop  20468  ucnprima  20513  tngtopn  20892  tgioo  21029  xrtgioo  21039  iccpnfcnv  21172  rrxip  21550  ovolicc2lem4  21659  nulmbl2  21675  iundisj  21686  dyadmax  21735  i1f1  21825  dvfval  22029  dvcnp2  22051  lhop1lem  22142  lhop2  22144  elqaalem1  22442  elqaalem3  22444  taylthlem2  22496  pserulm  22544  psercn2  22545  psercnlem2  22546  psercnlem1  22547  psercn  22548  pserdvlem1  22549  pserdvlem2  22550  pserdv  22551  pserdv2  22552  abelth  22563  dvlog  22753  efopnlem2  22759  logtayl  22762  cxpcn3lem  22842  cxpcn3  22843  resqrcn  22844  dvatan  22987  atancn  22988  rlimcnp  23016  rlimcnp2  23017  wilthlem3  23065  ftalem4  23070  ftalem5  23071  dchrisum0lem2a  23423  cchhllem  23859  axlowdimlem6  23919  choc1  25771  chub2i  25914  span0  25986  spanuni  25988  sshhococi  25990  chsup0  25992  spansnpji  26022  mayetes3i  26174  nlelshi  26505  pjimai  26621  pj3i  26653  shatomistici  26806  hatomistici  26807  atcvat4i  26842  iundisjf  26971  idssxp  26992  rinvf1o  26995  mptctf  27066  iundisjfi  27119  xrge0mulgnn0  27189  xrge0iifcnv  27401  xrge0iifiso  27403  xrge0iifhom  27405  esumfsupre  27567  esumpfinvallem  27570  esumpcvgval  27574  esumcvg  27582  measunl  27677  coinfliprv  27911  signsply0  27998  signstcl  28012  signstf  28013  kur14lem6  28145  nocvxminlem  28877  nocvxmin  28878  nobndlem1  28879  nobndlem2  28880  onint1  29341  oninhaus  29342  dvtan  29493  itg2addnclem2  29495  ftc1anclem6  29523  filnetlem3  29652  filnetlem4  29653  heiborlem3  29763  isdrngo2  29815  elrfi  30081  mapfzcons1  30104  eldioph4b  30200  dnnumch3lem  30449  dnnumch3  30450  dgraalem  30552  dgraaub  30555  rabexgf  30796  sumnnodd  30991  lptioo2cn  31006  lptioo1cn  31007  fourierdlem31  31257  fourierdlem102  31328  fourierdlem103  31329  fourierdlem104  31330  fourierdlem114  31340  fouriercn  31352  relopabVD  32656  bj-nuliotaALT  33543
  Copyright terms: Public domain W3C validator