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

Theorem sseqtri 3496
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 3489 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 211 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  sseqtr4i  3497  eqimssi  3518  abssi  3536  ssun2  3630  unixpss  4965  0ima  5200  fvssunirn  5901  difex2  6609  oelim2  7301  omopthlem2  7362  sbthlem7  7691  unifpw  7880  fiuni  7945  rankuni  8336  rankc2  8344  rankxpu  8349  rankmapu  8351  rankxplim  8352  infxpenlem  8446  cf0  8682  fin23lem17  8769  fin23lem31  8774  smobeth  9012  nqerf  9356  dmrecnq  9394  ackbijnn  13874  divalglem2  14361  divalglem2OLD  14362  divalglem5OLD  14364  divalglem5  14365  bitsfzolem  14395  bitsfzolemOLD  14396  0bits  14401  bezoutlem2OLD  14492  bezoutlem3OLD  14493  bezoutlem2  14495  bezoutlem3  14496  lcmcllem  14549  lcmledvds  14552  lcmscllemOLD  14570  lcmsledvdsOLD  14573  lcmfval  14579  lcmfvalOLD  14583  lcmfcllem  14586  lcmfledvds  14593  odzcllem  14725  odzdvds  14728  odzcllemOLD  14731  odzdvdsOLD  14734  unbenlem  14840  4sqlem13OLD  14889  4sqlem14OLD  14890  4sqlem17OLD  14893  4sqlem18OLD  14894  4sqlem13  14895  4sqlem14  14896  4sqlem17  14899  4sqlem18  14900  vdwlem8  14926  vdwnnlem3  14935  ramcl2lem  14950  ramcl2lemOLD  14951  ramtcl  14952  ramtclOLD  14953  ramtub  14956  ramtubOLD  14957  strle1  15209  prdsval  15341  xpsc0  15454  xpsc1  15455  wunfunc  15792  wunnat  15849  psssdm2  16449  tsrss  16457  gicer  16928  symgsssg  17096  symgfisg  17097  odlem2  17176  odlem2OLD  17192  gexlem2  17221  gexlem2OLD  17224  torsubg  17480  dprd2da  17663  zringlpirlem2OLD  19041  zringlpirlem3OLD  19042  zringlpirlem2  19043  zringlpirlem3  19044  pjfval  19256  pjpm  19258  eltg4i  19962  ntrss2  20059  isopn3  20069  mretopd  20095  leordtval2  20215  ptbasfi  20583  hmphtop  20780  hmpher  20786  restutop  21239  ucnprima  21284  tngtopn  21645  tgioo  21801  xrtgioo  21811  ovolicc2lem4OLD  22460  ovolicc2lem4  22461  nulmbl2  22477  iundisj  22488  dyadmax  22543  i1f1  22635  dvfval  22839  dvcnp2  22861  lhop1lem  22952  lhop2  22954  elqaalem1  23259  elqaalem3  23261  elqaalem1OLD  23262  elqaalem3OLD  23264  taylthlem2  23316  pserulm  23364  psercn2  23365  psercnlem2  23366  psercnlem1  23367  psercn  23368  pserdvlem1  23369  pserdvlem2  23370  pserdv  23371  pserdv2  23372  abelth  23383  dvlog  23583  efopnlem2  23589  logtayl  23592  cxpcn3lem  23674  cxpcn3  23675  resqrtcn  23676  dvatan  23848  atancn  23849  rlimcnp  23878  rlimcnp2  23879  wilthlem3  23982  ftalem4  23987  ftalem5  23988  ftalem4OLD  23989  ftalem5OLD  23990  dchrisum0lem2a  24342  cchhllem  24904  axlowdimlem6  24964  choc1  26966  chub2i  27109  span0  27181  spanuni  27183  sshhococi  27185  chsup0  27187  spansnpji  27217  mayetes3i  27368  nlelshi  27699  pjimai  27815  pj3i  27847  shatomistici  28000  hatomistici  28001  atcvat4i  28036  iundisjf  28189  mptexgf  28215  idssxp  28217  rinvf1o  28220  mptctf  28299  iundisjfi  28366  xrge0mulgnn0  28446  xrge0iifcnv  28735  xrge0iifiso  28737  xrge0iifhom  28739  esumcvgsum  28905  coinfliprv  29311  signsply0  29436  signstcl  29450  signstf  29451  kur14lem6  29930  mthmsta  30212  nocvxminlem  30572  nocvxmin  30573  nobndlem1  30574  nobndlem2  30575  filnetlem3  31029  filnetlem4  31030  onint1  31102  oninhaus  31103  bj-nuliotaALT  31579  imadifss  31842  poimirlem3  31857  poimirlem32  31886  dvtan  31906  itg2addnclem2  31908  ftc1anclem6  31936  heiborlem3  32059  isdrngo2  32111  elrfi  35455  mapfzcons1  35478  eldioph4b  35573  dnnumch3lem  35824  dnnumch3  35825  dgraalem  35927  dgraalemOLD  35928  dgraaub  35933  dgraaubOLD  35934  cotrcltrcl  36177  cotrclrcl  36194  frege131d  36216  binomcxplemdvbinom  36560  binomcxplemdvsum  36562  binomcxplemnotnn0  36563  relopabVD  37159  rabexgf  37206  fzssnn0  37381  iuneqfzuzlem  37399  sumnnodd  37530  lptioo2cn  37546  lptioo1cn  37547  fourierdlem31  37820  fourierdlem31OLD  37821  fourierdlem102  37892  fourierdlem114  37904  fouriercn  37916  elaa2lem  37917  elaa2lemOLD  37918  etransclem48OLD  37967  etransclem48  37968  sge0resplit  38036  caratheodorylem1  38126  hoicvr  38145  hoicvrrex  38153
  Copyright terms: Public domain W3C validator