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

Theorem sseqtri 3340
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 3333 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 200 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649    C_ wss 3280
This theorem is referenced by:  sseqtr4i  3341  eqimssi  3362  abssi  3378  ssun2  3471  difex2  4673  unixpss  4947  0ima  5181  fvssunirn  5713  oelim2  6797  omopthlem2  6858  sbthlem7  7182  unifpw  7367  fiuni  7391  rankuni  7745  rankc2  7753  rankxpu  7758  rankxplim  7759  infxpenlem  7851  cf0  8087  fin23lem17  8174  fin23lem31  8179  smobeth  8417  nqerf  8763  dmrecnq  8801  ackbijnn  12562  divalglem2  12870  divalglem5  12872  bitsfzolem  12901  0bits  12906  bezoutlem2  12994  bezoutlem3  12995  odzcllem  13133  odzdvds  13136  unbenlem  13231  4sqlem13  13280  4sqlem14  13281  4sqlem17  13284  4sqlem18  13285  vdwlem8  13311  vdwnnlem3  13320  ramcl2lem  13332  ramtcl  13333  ramtub  13335  strle1  13515  prdsval  13633  xpsc0  13740  xpsc1  13741  wunfunc  14051  wunnat  14108  psssdm2  14602  tsrss  14610  gicer  15018  odlem2  15132  gexlem2  15171  torsubg  15424  gsumzaddlem  15481  dprd2da  15555  zlpirlem2  16724  zlpirlem3  16725  pjfval  16888  pjpm  16890  eltg4i  16980  ntrss2  17076  isopn3  17085  mretopd  17111  leordtval2  17230  ptbasfi  17566  hmphtop  17763  hmpher  17769  restutop  18220  ucnprima  18265  tngtopn  18644  tgioo  18780  xrtgioo  18790  iccpnfcnv  18922  ovolicc2lem4  19369  nulmbl2  19384  iundisj  19395  dyadmax  19443  i1f1  19535  dvfval  19737  dvcnp2  19759  lhop1lem  19850  lhop2  19852  elqaalem1  20189  elqaalem3  20191  taylthlem2  20243  pserulm  20291  psercn2  20292  psercnlem2  20293  psercnlem1  20294  psercn  20295  pserdvlem1  20296  pserdvlem2  20297  pserdv  20298  pserdv2  20299  abelth  20310  dvlog  20495  efopnlem2  20501  logtayl  20504  cxpcn3lem  20584  cxpcn3  20585  resqrcn  20586  dvatan  20728  atancn  20729  rlimcnp  20757  rlimcnp2  20758  wilthlem2  20805  wilthlem3  20806  ftalem4  20811  ftalem5  20812  dchrisum0lem2a  21164  choc1  22782  chub2i  22925  span0  22997  spanuni  22999  sshhococi  23001  chsup0  23003  spansnpji  23033  mayetes3i  23185  nlelshi  23516  pjimai  23632  pj3i  23664  shatomistici  23817  hatomistici  23818  atcvat4i  23853  iundisjf  23982  rinvf1o  23995  mptctf  24065  iundisjfi  24105  xrge0mulgnn0  24163  xrge0adddir  24168  fsumrp0cl  24170  xrge0iifcnv  24272  xrge0iifiso  24274  xrge0iifhom  24276  lmlimxrge0  24287  rge0scvg  24288  lmdvg  24291  esumfsupre  24414  esumpfinvallem  24417  esumpfinval  24418  esumpfinvalf  24419  esumpcvgval  24421  esumcvg  24429  measunl  24523  coinfliprv  24693  kur14lem6  24850  nocvxminlem  25558  nocvxmin  25559  nobndlem1  25560  nobndlem2  25561  axlowdimlem6  25790  onint1  26103  oninhaus  26104  itg2addnclem2  26156  filnetlem3  26299  filnetlem4  26300  heiborlem3  26412  isdrngo2  26464  elrfi  26638  mapfzcons1  26663  eldioph4b  26762  dnnumch3lem  27011  dnnumch3  27012  dgraalem  27218  dgraaub  27221  symgsssg  27276  symgfisg  27277  rabexgf  27562  relopabVD  28722
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator