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

Theorem sseqtri 3464
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 3457 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 212 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1444    C_ wss 3404
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3411  df-ss 3418
This theorem is referenced by:  sseqtr4i  3465  eqimssi  3486  abssi  3504  ssun2  3598  unixpss  4949  0ima  5184  fvssunirn  5888  difex2  6598  oelim2  7296  omopthlem2  7357  sbthlem7  7688  unifpw  7877  fiuni  7942  rankuni  8334  rankc2  8342  rankxpu  8347  rankmapu  8349  rankxplim  8350  infxpenlem  8444  cf0  8681  fin23lem17  8768  fin23lem31  8773  smobeth  9011  nqerf  9355  dmrecnq  9393  ackbijnn  13886  divalglem2  14373  divalglem2OLD  14374  divalglem5OLD  14376  divalglem5  14377  bitsfzolem  14407  bitsfzolemOLD  14408  0bits  14413  bezoutlem2OLD  14504  bezoutlem3OLD  14505  bezoutlem2  14507  bezoutlem3  14508  lcmcllem  14561  lcmledvds  14564  lcmscllemOLD  14582  lcmsledvdsOLD  14585  lcmfval  14591  lcmfvalOLD  14595  lcmfcllem  14598  lcmfledvds  14605  odzcllem  14737  odzdvds  14740  odzcllemOLD  14743  odzdvdsOLD  14746  unbenlem  14852  4sqlem13OLD  14901  4sqlem14OLD  14902  4sqlem17OLD  14905  4sqlem18OLD  14906  4sqlem13  14907  4sqlem14  14908  4sqlem17  14911  4sqlem18  14912  vdwlem8  14938  vdwnnlem3  14947  ramcl2lem  14962  ramcl2lemOLD  14963  ramtcl  14964  ramtclOLD  14965  ramtub  14968  ramtubOLD  14969  strle1  15221  prdsval  15353  xpsc0  15466  xpsc1  15467  wunfunc  15804  wunnat  15861  psssdm2  16461  tsrss  16469  gicer  16940  symgsssg  17108  symgfisg  17109  odlem2  17188  odlem2OLD  17204  gexlem2  17233  gexlem2OLD  17236  torsubg  17492  dprd2da  17675  zringlpirlem2OLD  19054  zringlpirlem3OLD  19055  zringlpirlem2  19056  zringlpirlem3  19057  pjfval  19269  pjpm  19271  eltg4i  19975  ntrss2  20072  isopn3  20082  mretopd  20108  leordtval2  20228  ptbasfi  20596  hmphtop  20793  hmpher  20799  restutop  21252  ucnprima  21297  tngtopn  21658  tgioo  21814  xrtgioo  21824  ovolicc2lem4OLD  22473  ovolicc2lem4  22474  nulmbl2  22490  iundisj  22501  dyadmax  22556  i1f1  22648  dvfval  22852  dvcnp2  22874  lhop1lem  22965  lhop2  22967  elqaalem1  23272  elqaalem3  23274  elqaalem1OLD  23275  elqaalem3OLD  23277  taylthlem2  23329  pserulm  23377  psercn2  23378  psercnlem2  23379  psercnlem1  23380  psercn  23381  pserdvlem1  23382  pserdvlem2  23383  pserdv  23384  pserdv2  23385  abelth  23396  dvlog  23596  efopnlem2  23602  logtayl  23605  cxpcn3lem  23687  cxpcn3  23688  resqrtcn  23689  dvatan  23861  atancn  23862  rlimcnp  23891  rlimcnp2  23892  wilthlem3  23995  ftalem4  24000  ftalem5  24001  ftalem4OLD  24002  ftalem5OLD  24003  dchrisum0lem2a  24355  cchhllem  24917  axlowdimlem6  24977  choc1  26980  chub2i  27123  span0  27195  spanuni  27197  sshhococi  27199  chsup0  27201  spansnpji  27231  mayetes3i  27382  nlelshi  27713  pjimai  27829  pj3i  27861  shatomistici  28014  hatomistici  28015  atcvat4i  28050  iundisjf  28199  mptexgf  28225  idssxp  28227  rinvf1o  28230  mptctf  28305  iundisjfi  28372  xrge0mulgnn0  28451  xrge0iifcnv  28739  xrge0iifiso  28741  xrge0iifhom  28743  esumcvgsum  28909  coinfliprv  29315  signsply0  29440  signstcl  29454  signstf  29455  kur14lem6  29934  mthmsta  30216  nocvxminlem  30579  nocvxmin  30580  nobndlem1  30581  nobndlem2  30582  filnetlem3  31036  filnetlem4  31037  onint1  31109  oninhaus  31110  bj-nuliotaALT  31624  imadifss  31928  poimirlem3  31943  poimirlem32  31972  dvtan  31992  itg2addnclem2  31994  ftc1anclem6  32022  heiborlem3  32145  isdrngo2  32197  elrfi  35536  mapfzcons1  35559  eldioph4b  35654  dnnumch3lem  35904  dnnumch3  35905  dgraalem  36007  dgraalemOLD  36008  dgraaub  36013  dgraaubOLD  36014  resnonrel  36198  rtrclex  36224  rtrclexi  36228  cotrcltrcl  36317  cotrclrcl  36334  frege131d  36356  binomcxplemdvbinom  36702  binomcxplemdvsum  36704  binomcxplemnotnn0  36705  relopabVD  37298  rabexgf  37345  fzssnn0  37539  iuneqfzuzlem  37557  sumnnodd  37710  lptioo2cn  37726  lptioo1cn  37727  fourierdlem31  38000  fourierdlem31OLD  38001  fourierdlem102  38072  fourierdlem114  38084  fouriercn  38096  elaa2lem  38097  elaa2lemOLD  38098  etransclem48OLD  38147  etransclem48  38148  salexct  38193  salgencntex  38202  sge0resplit  38248  caratheodorylem1  38347  hoicvr  38370  hoicvrrex  38378  hoidmvlelem3  38419  hoidmvlelem4  38420
  Copyright terms: Public domain W3C validator