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

Theorem sseqtri 3223
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 3216 . 2  |-  ( A 
C_  B  <->  A  C_  C
)
41, 3mpbi 199 1  |-  A  C_  C
Colors of variables: wff set class
Syntax hints:    = wceq 1632    C_ wss 3165
This theorem is referenced by:  sseqtr4i  3224  eqimssi  3245  abssi  3261  ssun2  3352  difex2  4541  unixpss  4815  0ima  5047  fvssunirn  5567  oelim2  6609  omopthlem2  6670  sbthlem7  6993  unifpw  7174  fiuni  7197  rankuni  7551  rankc2  7559  rankxpu  7564  rankxplim  7565  infxpenlem  7657  cf0  7893  fin23lem17  7980  fin23lem31  7985  smobeth  8224  nqerf  8570  dmrecnq  8608  ackbijnn  12302  divalglem2  12610  divalglem5  12612  bitsfzolem  12641  0bits  12646  bezoutlem2  12734  bezoutlem3  12735  odzcllem  12873  odzdvds  12876  unbenlem  12971  4sqlem13  13020  4sqlem14  13021  4sqlem17  13024  4sqlem18  13025  vdwlem8  13051  vdwnnlem3  13060  ramcl2lem  13072  ramtcl  13073  ramtub  13075  strle1  13255  prdsval  13371  xpsc0  13478  xpsc1  13479  wunfunc  13789  wunnat  13846  psssdm2  14340  tsrss  14348  gicer  14756  odlem2  14870  gexlem2  14909  torsubg  15162  gsumzaddlem  15219  dprd2da  15293  zlpirlem2  16458  zlpirlem3  16459  pjfval  16622  pjpm  16624  eltg4i  16714  ntrss2  16810  isopn3  16819  mretopd  16845  leordtval2  16958  ptbasfi  17292  hmphtop  17485  hmpher  17491  tngtopn  18182  tgioo  18318  xrtgioo  18328  iccpnfcnv  18458  ovolicc2lem4  18895  nulmbl2  18910  iundisj  18921  dyadmax  18969  i1f1  19061  dvfval  19263  dvcnp2  19285  lhop1lem  19376  lhop2  19378  elqaalem1  19715  elqaalem3  19717  taylthlem2  19769  pserulm  19814  psercn2  19815  psercnlem2  19816  psercnlem1  19817  psercn  19818  pserdvlem1  19819  pserdvlem2  19820  pserdv  19821  pserdv2  19822  abelth  19833  dvlog  20014  efopnlem2  20020  logtayl  20023  cxpcn3lem  20103  cxpcn3  20104  resqrcn  20105  dvatan  20247  atancn  20248  rlimcnp  20276  rlimcnp2  20277  wilthlem2  20323  wilthlem3  20324  ftalem4  20329  ftalem5  20330  dchrisum0lem2a  20682  choc1  21922  chub2i  22065  span0  22137  spanuni  22139  sshhococi  22141  chsup0  22143  spansnpji  22173  mayetes3i  22325  nlelshi  22656  pjimai  22772  pj3i  22804  shatomistici  22957  hatomistici  22958  atcvat4i  22993  ballotlemfmpn  23069  xrge0mulgnn0  23328  xrge0iifcnv  23330  xrge0iifiso  23332  xrge0iifhom  23334  xrge0adddir  23347  fsumrp0cl  23349  mptctf  23363  iundisjfi  23378  iundisjf  23380  lmlimxrge0  23387  rge0scvg  23388  lmdvg  23391  esumpfinvallem  23457  esumpfinval  23458  esumpfinvalf  23459  esumpcvgval  23461  esumcvg  23469  coinfliprv  23698  kur14lem6  23757  nocvxminlem  24415  nocvxmin  24416  nobndlem1  24417  nobndlem2  24418  axlowdimlem6  24647  onint1  24960  oninhaus  24961  itg2addnclem2  25004  reldded  25844  relrded  25845  reldcat  25865  relrcat  25866  filnetlem3  26432  filnetlem4  26433  heiborlem3  26640  isdrngo2  26692  elrfi  26872  mapfzcons1  26897  eldioph4b  26997  dnnumch3lem  27246  dnnumch3  27247  dgraalem  27453  dgraaub  27456  symgsssg  27511  symgfisg  27512  rabexgf  27798  relopabVD  28993
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator