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

Theorem sseq1 3314
Description: Equality theorem for subclasses. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
sseq1  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )

Proof of Theorem sseq1
StepHypRef Expression
1 eqss 3308 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
2 sstr2 3300 . . . 4  |-  ( B 
C_  A  ->  ( A  C_  C  ->  B  C_  C ) )
32adantl 453 . . 3  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( A  C_  C  ->  B  C_  C )
)
4 sstr2 3300 . . . 4  |-  ( A 
C_  B  ->  ( B  C_  C  ->  A  C_  C ) )
54adantr 452 . . 3  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( B  C_  C  ->  A  C_  C )
)
63, 5impbid 184 . 2  |-  ( ( A  C_  B  /\  B  C_  A )  -> 
( A  C_  C  <->  B 
C_  C ) )
71, 6sylbi 188 1  |-  ( A  =  B  ->  ( A  C_  C  <->  B  C_  C
) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 177    /\ wa 359    = wceq 1649    C_ wss 3265
This theorem is referenced by:  sseq12  3316  sseq1i  3317  sseq1d  3320  nssne2  3350  psseq1  3379  uneqdifeq  3661  sbss  3682  pwjust  3745  elpw  3750  elpwg  3751  pwpw0  3891  sssn  3902  ssunsn2  3903  pwsnALT  3954  unimax  3993  trss  4254  elssabg  4298  intabs  4304  nnullss  4368  exss  4369  fri  4487  onssmin  4719  tfis  4776  tfisi  4780  releq  4901  xpsspw  4928  iss  5131  relcnvtr  5331  fununi  5459  funcnvuni  5460  ffoss  5649  ssimaex  5729  isofrlem  6001  f1oweALT  6015  frxp  6394  tfrlem1  6574  oawordeu  6736  qsss  6903  boxcutc  7043  sbthlem2  7156  sbth  7165  php  7229  isinf  7260  unbnn2  7302  domunfican  7317  fiint  7321  finsschain  7350  indexfi  7351  dffi3  7373  hartogslem1  7446  sucprcreg  7502  cantnfval2  7559  cantnfle  7561  cantnflem1  7580  tz9.1  7600  setind  7608  tcvalg  7612  scott0  7745  bnd2  7752  carduni  7803  cardaleph  7905  alephinit  7911  aceq3lem  7936  dfac12lem3  7960  infmap2  8033  cflem  8061  cflm  8065  cflecard  8068  cfeq0  8071  cfsuc  8072  cfflb  8074  cfslb  8081  cfslb2n  8083  coftr  8088  fin23lem13  8147  fin23lem16  8150  fin23lem19  8151  fin23lem29  8156  fin1a2lem13  8227  itunitc  8236  domtriomlem  8257  axdc3lem2  8266  zorn2lem7  8317  zornn0g  8320  fpwwe2lem5  8444  pwfseqlem4a  8471  pwfseqlem4  8472  wunfi  8531  wunex2  8548  wuncval  8552  rankcf  8587  tskuni  8593  axgroth6  8638  axgroth3  8641  axgroth4  8642  fzoss1  11094  hashf1lem2  11634  sumeq1f  12411  fsumcvg3  12452  fsum2d  12484  fsumabs  12509  fsumrlim  12519  fsumo1  12520  fsumiun  12529  vdwmc  13275  restsspw  13588  ismred2  13757  mrcval  13764  mrcuni  13775  acsfn  13813  isssc  13949  drsdirfi  14324  clatlem  14468  clatl  14472  ipodrsima  14520  cntzssv  15056  isslw  15171  sylow2alem2  15181  sylow2a  15182  efgval  15278  gsumzaddlem  15455  ablfac1eulem  15559  lspval  15980  lspindpi  16133  aspval  16316  mplsubglem  16427  mpllsslem  16428  mplcoe1  16457  mplcoe2  16459  znf1o  16757  zntoslem  16762  uniopn  16895  fiinopn  16899  fiinbas  16942  baspartn  16944  eltg2  16948  eltg3  16952  topbas  16962  pptbas  16997  clsval  17026  neival  17091  neiint  17093  neips  17102  opnneissb  17103  opnssneib  17104  innei  17114  neiptoptop  17120  neiptopnei  17121  restbas  17146  restcld  17160  neitr  17168  restcls  17169  restntr  17170  cnpdis  17281  nrmsep3  17343  cmpsublem  17386  cmpsub  17387  fiuncmp  17391  uncon  17415  1stcfb  17431  2ndc1stc  17437  1stcrest  17439  2ndcctbss  17441  2ndcomap  17444  dis2ndc  17446  lly1stc  17482  llycmpkgen2  17505  txbas  17522  eltx  17523  ptuni2  17531  neitx  17562  ptpjopn  17567  ptcld  17568  txlm  17603  tx1stc  17605  txkgen  17607  xkopt  17610  xkococnlem  17614  ptcmpfi  17768  fbssfi  17792  opnfbas  17797  isfil2  17811  isfildlem  17812  snfil  17819  fsubbas  17822  ssfg  17827  fgss2  17829  fgcl  17833  fbasrn  17839  fgtr  17845  ufli  17869  uffix  17876  rnelfmlem  17907  fclscf  17980  alexsublem  17998  alexsubALTlem2  18002  alexsubALTlem3  18003  alexsubALTlem4  18004  alexsubALT  18005  tmdgsum2  18049  subgntr  18059  opnsubg  18060  divstgpopn  18072  tsmsfbas  18080  tsmsgsum  18091  tsmsres  18096  tsmsf1o  18097  tsmsxplem1  18105  tsmsxp  18107  isust  18156  ustssel  18158  ustincl  18160  ustdiag  18161  ustinvel  18162  ustexhalf  18163  ustexsym  18168  ust0  18172  restutop  18190  ustuqtop4  18197  utopsnneiplem  18200  blssex  18349  neibl  18423  blcld  18427  met1stc  18443  met2ndci  18444  metrest  18446  prdsxmslem2  18451  metustfbas  18479  cfilucfil  18481  metuel2  18487  metustbl  18488  restmetu  18491  dscopn  18494  isngp2  18517  tgioo  18700  tgqioo  18704  zdis  18720  xrge0tsms  18738  fsumcn  18773  ovolval  19239  volivth  19368  vitalilem2  19370  itgfsum  19587  limcun  19651  recnprss  19660  dvmptfsum  19728  ftc1a  19790  plyssc  19988  efopn  20418  jensen  20696  usgraedgprv  21265  hhsssh  22619  shintcl  22682  chintcl  22684  spanval  22685  omlsi  22756  pjoml  22788  chnlen0  22796  chsscon3  22852  chlejb1  22864  chnle  22866  spanun  22897  h1datom  22934  cmbr4i  22953  pjoml2  22963  pjoml3  22964  lecm  22969  osumcor2i  22996  osum  22997  spansncv  23005  pjcjt2  23044  pjopyth  23072  hstel2  23572  stj  23588  stcltr1i  23627  mdi  23648  mdbr3  23650  mdbr4  23651  dmdbr  23652  dmdmd  23653  dmdbr5  23661  mdsl1i  23674  mdslmd1lem3  23680  mdslmd1lem4  23681  mdslmd1i  23682  csmdsymi  23687  atss  23699  atom1d  23706  superpos  23707  chcv1  23708  shatomici  23711  shatomistici  23714  hatomistici  23715  chrelat2  23723  chirredi  23747  atcvat4i  23750  mdsymlem2  23757  mdsymlem6  23761  dmdbr6ati  23776  dmdbr7ati  23777  xrge0tsmsd  24054  tpr2rico  24116  issiga  24292  isrnsigaOLD  24293  isrnsiga  24294  sigagenval  24321  measiuns  24367  dya2icoseg  24423  dya2iocnrect  24427  dya2iocuni  24429  kur14lem1  24673  cvmopnlem  24746  rtrclreclem.min  24928  prodeq1f  25015  dfon2lem3  25167  dfon2lem7  25171  frmin  25268  wfrlem1  25282  wfrlem4  25285  wfrlem15  25296  frrlem1  25307  frrlem3  25309  brsset  25455  bpolyval  25811  onsucsuccmpi  25909  ovoliunnfl  25955  voliunnfl  25957  volsupnfl  25958  refssex  26054  fness  26055  fneref  26057  fnessref  26066  neibastop2lem  26082  topmeet  26086  fnejoin2  26091  tailfb  26099  filnetlem4  26103  indexa  26128  indexdom  26129  neificl  26152  istotbnd3  26173  sstotbnd2  26176  sstotbnd  26177  equivtotbnd  26180  ssbnd  26190  heiborlem1  26213  heiborlem6  26218  heiborlem8  26220  heiborlem10  26222  unichnidl  26334  pridl  26340  ismaxidl  26343  igenval  26364  igenval2  26369  ispridlc  26373  ismrcd1  26445  ismrcd2  26446  ismrc  26448  mzpcompact2lem  26501  aomclem6  26827  hbtlem6  27004  rgspnval  27044  pmtrfrn  27071  stoweidlem51  27470  stoweidlem52  27471  frisusgranb  27752  onfrALTlem5  27973  onfrALTlem5VD  28340  bnj517  28596  bnj1118  28693  bnj1145  28702  bnj1154  28708  bnj1452  28761  bnj1498  28770  lsmsat  29125  lssatomic  29128  lssats  29129  lsat0cv  29150  lcvexchlem4  29154  lcvexchlem5  29155  lsatcvatlem  29166  l1cvpat  29171  ispsubsp  29861  linepsubN  29868  pclvalN  30006  ispsubclN  30053  ispsubcl2N  30063  pclfinclN  30066  diaelrnN  31162  docavalN  31240  dochval  31468  dvh4dimat  31555  dochexmidlem1  31577  lpolconN  31604  mapdordlem2  31754
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2370
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 2376  df-cleq 2382  df-clel 2385  df-in 3272  df-ss 3279
  Copyright terms: Public domain W3C validator