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

Theorem sseq1 3524
Description: Equality theorem for subclasses. (Contributed by NM, 24-Jun-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
sseq1

Proof of Theorem sseq1
StepHypRef Expression
1 eqss 3518 . 2
2 sstr2 3510 . . . 4
32adantl 466 . . 3
4 sstr2 3510 . . . 4
54adantr 465 . . 3
63, 5impbid 191 . 2
71, 6sylbi 195 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  /\wa 369  =wceq 1395  C_wss 3475
This theorem is referenced by:  sseq12  3526  sseq1i  3527  sseq1d  3530  nssne2  3560  psseq1  3590  uneqdifeq  3916  sbss  3939  pwjust  4013  elpw  4018  elpwg  4020  pwpw0  4178  sssn  4188  ssunsn2  4189  pwsnALT  4244  unimax  4285  trss  4554  sseliALT  4583  elssabg  4607  intabs  4613  nnullss  4714  exss  4715  fri  4846  releq  5090  xpsspw  5121  iss  5326  relcnvtr  5532  fununi  5659  ssimaex  5938  isofrlem  6236  onssmin  6632  tfis  6689  tfisi  6693  funcnvuni  6753  ffoss  6761  f1oweALT  6784  frxp  6910  tfrlem1  7064  oawordeu  7223  qsss  7391  boxcutc  7532  sbthlem2  7648  sbth  7657  php  7721  isinf  7753  findcard2d  7782  unbnn2  7797  domunfican  7813  fiint  7817  finsschain  7847  indexfi  7848  dffi3  7911  hartogslem1  7988  sucprcregOLD  8047  cantnfval2  8109  cantnfle  8111  cantnflem1  8129  cantnfval2OLD  8139  cantnfleOLD  8141  cantnflem1OLD  8152  tz9.1  8181  setind  8186  tcvalg  8190  scott0  8325  bnd2  8332  carduni  8383  cardaleph  8491  alephinit  8497  aceq3lem  8522  dfac12lem3  8546  infmap2  8619  cflem  8647  cflm  8651  cflecard  8654  cfeq0  8657  cfsuc  8658  cfflb  8660  cfslb  8667  cfslb2n  8669  coftr  8674  fin23lem13  8733  fin23lem16  8736  fin23lem19  8737  fin23lem29  8742  fin1a2lem13  8813  itunitc  8822  domtriomlem  8843  axdc3lem2  8852  zorn2lem7  8903  zornn0g  8906  fpwwe2lem5  9033  pwfseqlem4a  9060  pwfseqlem4  9061  wunfi  9120  wunex2  9137  wuncval  9141  rankcf  9176  tskuni  9182  axgroth6  9227  axgroth3  9230  axgroth4  9231  fzoss1  11852  fsuppmapnn0fiubex  12098  hashf1lem2  12505  sumeq1  13511  fsumcvg3  13551  fsum2d  13586  fsumabs  13615  fsumrlim  13625  fsumo1  13626  fsumiun  13635  prodeq1f  13715  fprod2d  13785  vdwmc  14496  restsspw  14829  ismred2  15000  mrcval  15007  mrcuni  15018  acsfn  15056  isssc  15189  drsdirfi  15567  ipodrsima  15795  cntzssv  16366  pmtrfrn  16483  pmtrrn2  16485  pmtrdifellem1  16501  pmtrdifellem2  16502  isslw  16628  sylow2alem2  16638  sylow2a  16639  efgval  16735  gsumzaddlem  16934  gsumzaddlemOLD  16936  ablfac1eulem  17123  lspval  17621  lspindpi  17778  aspval  17977  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  znf1o  18590  zntoslem  18595  mdetunilem9  19122  uniopn  19406  fiinopn  19410  fiinbas  19453  baspartn  19455  eltg2  19459  eltg3  19463  topbas  19474  pptbas  19509  clsval  19538  neival  19603  neiint  19605  neips  19614  opnneissb  19615  opnssneib  19616  innei  19626  neiptoptop  19632  neiptopnei  19633  restbas  19659  restcld  19673  neitr  19681  restcls  19682  restntr  19683  cnpdis  19794  nrmsep3  19856  cmpsublem  19899  cmpsub  19900  fiuncmp  19904  uncon  19930  1stcfb  19946  2ndc1stc  19952  1stcrest  19954  2ndcctbss  19956  2ndcomap  19959  dis2ndc  19961  lly1stc  19997  refssex  20012  refun0  20016  llycmpkgen2  20051  txbas  20068  eltx  20069  ptuni2  20077  neitx  20108  ptpjopn  20113  ptcld  20114  txlm  20149  tx1stc  20151  txkgen  20153  xkopt  20156  xkococnlem  20160  ptcmpfi  20314  fbssfi  20338  opnfbas  20343  isfil2  20357  isfildlem  20358  snfil  20365  fsubbas  20368  ssfg  20373  fgss2  20375  fgcl  20379  fbasrn  20385  fgtr  20391  ufli  20415  uffix  20422  rnelfmlem  20453  fclscf  20526  alexsublem  20544  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  tmdgsum2  20595  subgntr  20605  opnsubg  20606  qustgpopn  20618  tsmsfbas  20626  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmsf1o  20647  tsmsxplem1  20655  tsmsxp  20657  isust  20706  ustssel  20708  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  ustexsym  20718  ust0  20722  restutop  20740  ustuqtop4  20747  utopsnneiplem  20750  blssexps  20929  blssex  20930  neibl  21004  blcld  21008  met1stc  21024  met2ndci  21025  metrest  21027  prdsxmslem2  21032  metustfbasOLD  21068  metustfbas  21069  cfilucfilOLD  21072  cfilucfil  21073  metuel2  21082  metustblOLD  21083  metustbl  21084  restmetu  21090  dscopn  21094  isngp2  21117  tgioo  21301  tgqioo  21305  zdis  21321  xrge0tsms  21339  fsumcn  21374  ovolval  21885  volivth  22016  vitalilem2  22018  itgfsum  22233  limcun  22299  recnprss  22308  dvmptfsum  22376  ftc1a  22438  plyssc  22597  efopn  23039  jensen  23318  tglnunirn  23935  usgraedgprv  24376  frisusgranb  24997  hhsssh  26185  shintcl  26248  chintcl  26250  spanval  26251  omlsi  26322  pjoml  26354  chnlen0  26362  chsscon3  26418  chlejb1  26430  chnle  26432  spanun  26463  h1datom  26500  cmbr4i  26519  pjoml2  26529  pjoml3  26530  lecm  26535  osumcor2i  26562  osum  26563  spansncv  26571  pjcjt2  26610  pjopyth  26638  hstel2  27138  stj  27154  stcltr1i  27193  mdi  27214  mdbr3  27216  mdbr4  27217  dmdbr  27218  dmdmd  27219  dmdbr5  27227  mdsl1i  27240  mdslmd1lem3  27246  mdslmd1lem4  27247  mdslmd1i  27248  csmdsymi  27253  atss  27265  atom1d  27272  superpos  27273  chcv1  27274  shatomici  27277  shatomistici  27280  hatomistici  27281  chrelat2  27289  chirredi  27313  atcvat4i  27316  mdsymlem2  27323  mdsymlem6  27327  dmdbr6ati  27342  dmdbr7ati  27343  gsumle  27770  gsumvsca1  27773  gsumvsca2  27774  xrge0tsmsd  27775  tpr2rico  27894  issiga  28111  isrnsigaOLD  28112  isrnsiga  28113  sigagenval  28140  measiuns  28188  dya2icoseg  28248  dya2iocnrect  28252  dya2iocuni  28254  kur14lem1  28650  cvmopnlem  28723  rtrclreclem.min  29070  dfon2lem3  29217  dfon2lem7  29221  frmin  29322  wfrlem1  29343  wfrlem4  29346  wfrlem15  29357  frrlem1  29387  frrlem3  29389  brsset  29539  onsucsuccmpi  29908  mblfinlem2  30052  mblfinlem3  30053  mblfinlem4  30054  ismblfin  30055  ovoliunnfl  30056  voliunnfl  30058  volsupnfl  30059  fness  30167  fneref  30168  fnessref  30175  neibastop2lem  30178  topmeet  30182  fnejoin2  30187  tailfb  30195  filnetlem4  30199  indexa  30224  indexdom  30225  neificl  30246  istotbnd3  30267  sstotbnd2  30270  sstotbnd  30271  equivtotbnd  30274  ssbnd  30284  heiborlem1  30307  heiborlem6  30312  heiborlem8  30314  heiborlem10  30316  unichnidl  30428  pridl  30434  ismaxidl  30437  igenval  30458  igenval2  30463  ispridlc  30467  ismrcd1  30630  ismrcd2  30631  ismrc  30633  mzpcompact2lem  30684  aomclem6  31005  hbtlem6  31078  rgspnval  31117  islptre  31625  dvmptconst  31710  dvmptidg  31712  dvmulcncf  31722  dvdivcncf  31724  dvmptfprod  31742  stoweidlem51  31833  stoweidlem52  31834  fourierdlem103  31992  fourierdlem104  31993  onfrALTlem5  33314  onfrALTlem5VD  33685  bnj517  33943  bnj1118  34040  bnj1145  34049  bnj1154  34055  bnj1452  34108  bnj1498  34117  bj-snglss  34528  lsmsat  34733  lssatomic  34736  lssats  34737  lsat0cv  34758  lcvexchlem4  34762  lcvexchlem5  34763  lsatcvatlem  34774  l1cvpat  34779  ispsubsp  35469  linepsubN  35476  pclvalN  35614  ispsubclN  35661  ispsubcl2N  35671  pclfinclN  35674  diaelrnN  36772  docavalN  36850  dochval  37078  dvh4dimat  37165  dochexmidlem1  37187  lpolconN  37214  mapdordlem2  37364  ssficl  37754  ssuncl  37755  ssdifcl  37756  sssymdifcl  37757
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator