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

Theorem sseqtri 3486
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 3479 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 208 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370    C_ wss 3426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3433  df-ss 3440
This theorem is referenced by:  sseqtr4i  3487  eqimssi  3508  abssi  3525  ssun2  3618  unixpss  5053  0ima  5283  fvssunirn  5812  difex2  6483  oelim2  7134  omopthlem2  7195  sbthlem7  7527  unifpw  7715  fiuni  7779  rankuni  8171  rankc2  8179  rankxpu  8184  rankmapu  8186  rankxplim  8187  infxpenlem  8281  cf0  8521  fin23lem17  8608  fin23lem31  8613  smobeth  8851  nqerf  9200  dmrecnq  9238  ackbijnn  13393  divalglem2  13701  divalglem5  13703  bitsfzolem  13732  0bits  13737  bezoutlem2  13825  bezoutlem3  13826  odzcllem  13966  odzdvds  13969  unbenlem  14071  4sqlem13  14120  4sqlem14  14121  4sqlem17  14124  4sqlem18  14125  vdwlem8  14151  vdwnnlem3  14160  ramcl2lem  14172  ramtcl  14173  ramtub  14175  strle1  14371  prdsval  14495  xpsc0  14600  xpsc1  14601  wunfunc  14911  wunnat  14968  psssdm2  15487  tsrss  15495  gicer  15906  symgsssg  16075  symgfisg  16076  odlem2  16146  gexlem2  16185  torsubg  16440  gsumzaddlemOLD  16514  dprd2da  16646  zringlpirlem2  18013  zringlpirlem3  18014  zlpirlem2  18018  zlpirlem3  18019  pjfval  18240  pjpm  18242  frlmip  18312  eltg4i  18681  ntrss2  18777  isopn3  18786  mretopd  18812  leordtval2  18932  ptbasfi  19270  hmphtop  19467  hmpher  19473  restutop  19928  ucnprima  19973  tngtopn  20352  tgioo  20489  xrtgioo  20499  iccpnfcnv  20632  rrxip  21010  ovolicc2lem4  21119  nulmbl2  21134  iundisj  21145  dyadmax  21194  i1f1  21284  dvfval  21488  dvcnp2  21510  lhop1lem  21601  lhop2  21603  elqaalem1  21901  elqaalem3  21903  taylthlem2  21955  pserulm  22003  psercn2  22004  psercnlem2  22005  psercnlem1  22006  psercn  22007  pserdvlem1  22008  pserdvlem2  22009  pserdv  22010  pserdv2  22011  abelth  22022  dvlog  22212  efopnlem2  22218  logtayl  22221  cxpcn3lem  22301  cxpcn3  22302  resqrcn  22303  dvatan  22446  atancn  22447  rlimcnp  22475  rlimcnp2  22476  wilthlem3  22524  ftalem4  22529  ftalem5  22530  dchrisum0lem2a  22882  cchhllem  23268  axlowdimlem6  23328  choc1  24865  chub2i  25008  span0  25080  spanuni  25082  sshhococi  25084  chsup0  25086  spansnpji  25116  mayetes3i  25268  nlelshi  25599  pjimai  25715  pj3i  25747  shatomistici  25900  hatomistici  25901  atcvat4i  25936  iundisjf  26065  rinvf1o  26083  mptctf  26155  iundisjfi  26214  xrge0mulgnn0  26284  gsumle  26380  xrge0iifcnv  26497  xrge0iifiso  26499  xrge0iifhom  26501  esumfsupre  26654  esumpfinvallem  26657  esumpcvgval  26661  esumcvg  26669  measunl  26764  coinfliprv  26999  signsply0  27086  signstcl  27100  signstf  27101  kur14lem6  27233  nocvxminlem  27965  nocvxmin  27966  nobndlem1  27967  nobndlem2  27968  onint1  28429  oninhaus  28430  dvtan  28580  itg2addnclem2  28582  ftc1anclem6  28610  filnetlem3  28739  filnetlem4  28740  heiborlem3  28850  isdrngo2  28902  elrfi  29168  mapfzcons1  29191  eldioph4b  29288  dnnumch3lem  29537  dnnumch3  29538  dgraalem  29640  dgraaub  29643  rabexgf  29884  relopabVD  31937  bj-nuliotaALT  32822
  Copyright terms: Public domain W3C validator