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

Theorem sseqtri 3531
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 3524 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 208 1  |-  A  C_  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1395    C_ wss 3471
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3478  df-ss 3485
This theorem is referenced by:  sseqtr4i  3532  eqimssi  3553  abssi  3571  ssun2  3664  unixpss  5127  0ima  5363  fvssunirn  5895  difex2  6606  oelim2  7262  omopthlem2  7323  sbthlem7  7652  unifpw  7841  fiuni  7906  rankuni  8298  rankc2  8306  rankxpu  8311  rankmapu  8313  rankxplim  8314  infxpenlem  8408  cf0  8648  fin23lem17  8735  fin23lem31  8740  smobeth  8978  nqerf  9325  dmrecnq  9363  ackbijnn  13652  divalglem2  14065  divalglem5  14067  bitsfzolem  14096  0bits  14101  bezoutlem2  14189  bezoutlem3  14190  odzcllem  14331  odzdvds  14334  unbenlem  14438  4sqlem13  14487  4sqlem14  14488  4sqlem17  14491  4sqlem18  14492  vdwlem8  14518  vdwnnlem3  14527  ramcl2lem  14539  ramtcl  14540  ramtub  14542  strle1  14743  prdsval  14872  xpsc0  14977  xpsc1  14978  wunfunc  15315  wunnat  15372  psssdm2  15972  tsrss  15980  gicer  16451  symgsssg  16619  symgfisg  16620  odlem2  16690  gexlem2  16729  torsubg  16987  gsumzaddlemOLD  17063  dprd2da  17218  zringlpirlem2  18637  zringlpirlem3  18638  zlpirlem2  18642  zlpirlem3  18643  pjfval  18864  pjpm  18866  eltg4i  19588  ntrss2  19685  isopn3  19694  mretopd  19720  leordtval2  19840  ptbasfi  20208  hmphtop  20405  hmpher  20411  restutop  20866  ucnprima  20911  tngtopn  21290  tgioo  21427  xrtgioo  21437  ovolicc2lem4  22057  nulmbl2  22073  iundisj  22084  dyadmax  22133  i1f1  22223  dvfval  22427  dvcnp2  22449  lhop1lem  22540  lhop2  22542  elqaalem1  22841  elqaalem3  22843  taylthlem2  22895  pserulm  22943  psercn2  22944  psercnlem2  22945  psercnlem1  22946  psercn  22947  pserdvlem1  22948  pserdvlem2  22949  pserdv  22950  pserdv2  22951  abelth  22962  dvlog  23158  efopnlem2  23164  logtayl  23167  cxpcn3lem  23247  cxpcn3  23248  resqrtcn  23249  dvatan  23392  atancn  23393  rlimcnp  23421  rlimcnp2  23422  wilthlem3  23470  ftalem4  23475  ftalem5  23476  dchrisum0lem2a  23828  cchhllem  24317  axlowdimlem6  24377  choc1  26372  chub2i  26515  span0  26587  spanuni  26589  sshhococi  26591  chsup0  26593  spansnpji  26623  mayetes3i  26775  nlelshi  27106  pjimai  27222  pj3i  27254  shatomistici  27407  hatomistici  27408  atcvat4i  27443  iundisjf  27588  mptexgf  27614  idssxp  27616  rinvf1o  27619  mptctf  27701  iundisjfi  27761  xrge0mulgnn0  27837  xrge0iifcnv  28076  xrge0iifiso  28078  xrge0iifhom  28080  esumcvgsum  28260  coinfliprv  28618  signsply0  28705  signstcl  28719  signstf  28720  kur14lem6  28852  mthmsta  29135  nocvxminlem  29667  nocvxmin  29668  nobndlem1  29669  nobndlem2  29670  onint1  30119  oninhaus  30120  dvtan  30270  itg2addnclem2  30272  ftc1anclem6  30300  filnetlem3  30403  filnetlem4  30404  heiborlem3  30514  isdrngo2  30566  elrfi  30831  mapfzcons1  30854  eldioph4b  30949  dnnumch3lem  31196  dnnumch3  31197  dgraalem  31298  dgraaub  31301  lcmcllem  31406  lcmledvds  31409  binomcxplemdvbinom  31462  binomcxplemdvsum  31464  binomcxplemnotnn0  31465  rabexgf  31602  fzssnn0  31725  sumnnodd  31839  lptioo2cn  31854  lptioo1cn  31855  fourierdlem31  32123  fourierdlem102  32194  fourierdlem114  32206  fouriercn  32218  elaa2lem  32219  etransclem48  32268  relopabVD  33844  bj-nuliotaALT  34730
  Copyright terms: Public domain W3C validator