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

Theorem sseqtri 3376
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 3369 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 208 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  sseqtr4i  3377  eqimssi  3398  abssi  3415  ssun2  3508  unixpss  4942  0ima  5173  fvssunirn  5701  difex2  6372  oelim2  7022  omopthlem2  7083  sbthlem7  7415  unifpw  7602  fiuni  7666  rankuni  8058  rankc2  8066  rankxpu  8071  rankmapu  8073  rankxplim  8074  infxpenlem  8168  cf0  8408  fin23lem17  8495  fin23lem31  8500  smobeth  8738  nqerf  9087  dmrecnq  9125  ackbijnn  13274  divalglem2  13582  divalglem5  13584  bitsfzolem  13613  0bits  13618  bezoutlem2  13706  bezoutlem3  13707  odzcllem  13847  odzdvds  13850  unbenlem  13952  4sqlem13  14001  4sqlem14  14002  4sqlem17  14005  4sqlem18  14006  vdwlem8  14032  vdwnnlem3  14041  ramcl2lem  14053  ramtcl  14054  ramtub  14056  strle1  14252  prdsval  14376  xpsc0  14481  xpsc1  14482  wunfunc  14792  wunnat  14849  psssdm2  15368  tsrss  15376  gicer  15784  symgsssg  15953  symgfisg  15954  odlem2  16022  gexlem2  16061  torsubg  16316  gsumzaddlemOLD  16390  dprd2da  16515  zringlpirlem2  17746  zringlpirlem3  17747  zlpirlem2  17751  zlpirlem3  17752  pjfval  17973  pjpm  17975  frlmip  18045  eltg4i  18407  ntrss2  18503  isopn3  18512  mretopd  18538  leordtval2  18658  ptbasfi  18996  hmphtop  19193  hmpher  19199  restutop  19654  ucnprima  19699  tngtopn  20078  tgioo  20215  xrtgioo  20225  iccpnfcnv  20358  rrxip  20736  ovolicc2lem4  20845  nulmbl2  20860  iundisj  20871  dyadmax  20920  i1f1  21010  dvfval  21214  dvcnp2  21236  lhop1lem  21327  lhop2  21329  elqaalem1  21670  elqaalem3  21672  taylthlem2  21724  pserulm  21772  psercn2  21773  psercnlem2  21774  psercnlem1  21775  psercn  21776  pserdvlem1  21777  pserdvlem2  21778  pserdv  21779  pserdv2  21780  abelth  21791  dvlog  21981  efopnlem2  21987  logtayl  21990  cxpcn3lem  22070  cxpcn3  22071  resqrcn  22072  dvatan  22215  atancn  22216  rlimcnp  22244  rlimcnp2  22245  wilthlem3  22293  ftalem4  22298  ftalem5  22299  dchrisum0lem2a  22651  cchhllem  22956  axlowdimlem6  23016  choc1  24553  chub2i  24696  span0  24768  spanuni  24770  sshhococi  24772  chsup0  24774  spansnpji  24804  mayetes3i  24956  nlelshi  25287  pjimai  25403  pj3i  25435  shatomistici  25588  hatomistici  25589  atcvat4i  25624  iundisjf  25755  rinvf1o  25773  mptctf  25845  iundisjfi  25903  xrge0mulgnn0  25973  rge0ssre  25978  gsumle  26098  xrge0iifcnv  26217  xrge0iifiso  26219  xrge0iifhom  26221  esumfsupre  26374  esumpfinvallem  26377  esumpcvgval  26381  esumcvg  26389  measunl  26484  coinfliprv  26713  signsply0  26800  signstcl  26814  signstf  26815  kur14lem6  26947  nocvxminlem  27678  nocvxmin  27679  nobndlem1  27680  nobndlem2  27681  onint1  28143  oninhaus  28144  dvtan  28286  itg2addnclem2  28288  ftc1anclem6  28316  filnetlem3  28445  filnetlem4  28446  heiborlem3  28556  isdrngo2  28608  elrfi  28875  mapfzcons1  28898  eldioph4b  28995  dnnumch3lem  29244  dnnumch3  29245  dgraalem  29347  dgraaub  29350  rabexgf  29591  relopabVD  31339
  Copyright terms: Public domain W3C validator