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

Theorem sseq2 3525
Description: Equality theorem for the subclass relationship. (Contributed by NM, 25-Jun-1998.)
Assertion
Ref Expression
sseq2

Proof of Theorem sseq2
StepHypRef Expression
1 sstr2 3510 . . . 4
21com12 31 . . 3
3 sstr2 3510 . . . 4
43com12 31 . . 3
52, 4anim12i 566 . 2
6 eqss 3518 . 2
7 dfbi2 628 . 2
85, 6, 73imtr4i 266 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  sseq2i  3528  sseq2d  3531  syl5sseq  3551  nssne1  3559  psseq2  3591  sseq0  3817  un00  3862  disjpss  3877  pweq  4015  ssintab  4303  ssintub  4304  intmin  4306  treq  4551  sseliALT  4583  ssexg  4598  intabs  4613  ordunidif  4931  ordssun  4982  fununi  5659  feq3  5720  ssimaexg  5939  iunpw  6614  tfindsg  6695  limomss  6705  findsg  6727  funcnvuni  6753  frxp  6910  onfununi  7031  oawordeu  7223  oawordexr  7224  nnawordex  7305  ereq1  7337  xpider  7401  domeng  7550  sbthlem4  7650  sbthlem5  7651  domssex  7698  finsschain  7847  dffi2  7903  dffi3  7911  hartogslem1  7988  inf3lema  8062  cantnflem1  8129  cantnflem1OLD  8152  tz9.1  8181  tz9.1c  8182  tctr  8192  tcmin  8193  tcrank  8323  scottex  8324  cardlim  8374  infxpenlem  8412  infxpenc2  8420  infxpenc2OLD  8424  isinfcard  8494  alephinit  8497  alephval3  8512  dfac3  8523  cflem  8647  cfval  8648  cflecard  8654  cfsuc  8658  cff1  8659  cfflb  8660  cflim2  8664  isf32lem2  8755  fin1a2lem13  8813  ac7g  8875  ttukeylem5  8914  ttukeylem7  8916  pwcfsdom  8979  pwfseqlem5  9062  pwfseq  9063  gch2  9074  winalim  9094  wunex  9138  wuncss  9144  eltskg  9149  eltsk2g  9150  gruina  9217  grur1a  9218  axgroth6  9227  swrdvalodm2  12664  swrdvalodm  12665  fprodss  13755  mrcflem  15003  mrcval  15007  isacs2  15050  acsfiel  15051  ipoval  15784  fpwipodrs  15794  ipodrsima  15795  mreclatBAD  15817  slwispgp  16631  pgpssslw  16634  lsmss1b  16685  lsmss2b  16687  cntzcmnss  16849  gsumzres  16914  lspf  17620  lspval  17621  lbsextlem1  17804  lbsextlem3  17806  lbsextlem4  17807  aspval  17977  mplsubglem  18093  mpllsslem  18094  mplsubglemOLD  18095  mpllsslemOLD  18096  basis2  19452  eltg2  19459  clsval  19538  clscld  19548  clsval2  19551  ntrcls0  19577  isnei  19604  neiint  19605  neips  19614  opnneissb  19615  opnssneib  19616  neindisj2  19624  innei  19626  neiptoptop  19632  neiptopnei  19633  neitr  19681  restcls  19682  cnpimaex  19757  cnprest2  19791  regsep  19835  nrmsep3  19856  nrmsep  19858  regsep2  19877  tgcmp  19901  uncmp  19903  bwth  19910  bwthOLD  19911  1stcfb  19946  1stcrest  19954  2ndcctbss  19956  1stcelcls  19962  lly1stc  19997  ssref  20013  refref  20014  comppfsc  20033  xkoopn  20090  neitx  20108  txcnp  20121  txcmplem1  20142  kqnrmlem1  20244  kqnrmlem2  20245  nrmhmph  20295  fbssfi  20338  opnfbas  20343  fbasfip  20369  fbunfip  20370  fgss2  20375  fgcl  20379  supfil  20396  isufil2  20409  filssufilg  20412  ssufl  20419  ufileu  20420  elfm3  20451  fmfnfm  20459  ufldom  20463  fbflim2  20478  flfneii  20493  flftg  20497  txflf  20507  supnfcls  20521  fclscf  20526  fclsfnflim  20528  flimfnfcls  20529  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  tsmsfbas  20626  tsmsresOLD  20645  tsmsres  20646  tsmsf1o  20647  tsmsxplem1  20655  tsmsxp  20657  ustssel  20708  ustincl  20710  ustdiag  20711  ustinvel  20712  ustexhalf  20713  ust0  20722  elutop  20736  ustuqtop4  20747  cfiluexsm  20793  cfiluweak  20798  blssps  20927  blss  20928  metss  21011  metrest  21027  metcnp3  21043  metnrmlem3  21365  lebnumlem3  21463  lebnum  21464  ellimc3  22283  lhop1lem  22414  dchrelbas  23511  avril1  25171  resgrprn  25282  spanval  26251  spancl  26254  shsval2i  26305  omlsi  26322  ococin  26326  chsupsn  26331  pjoml  26354  shs00i  26368  chj00i  26405  chsscon3  26418  chlejb1  26430  chnle  26432  pjoml2  26529  pjoml3  26530  lecm  26535  stcltr1i  27193  mdbr  27213  dmdmd  27219  dmdi  27221  dmdbr3  27224  dmdbr4  27225  mdsl1i  27240  mdslmd1lem3  27246  mdslmd1lem4  27247  csmdsymi  27253  hatomic  27279  chrelat2  27289  atord  27307  atcvat4i  27316  reff  27842  cmpcref  27853  sigagenval  28140  dmsigagen  28144  sigagenss  28149  kur14lem9  28658  mclsssvlem  28922  mclsind  28930  dfrtrcl2  29071  wrecseq123  29337  wfrlem1  29343  wfrlem4  29346  wfrlem15  29357  frrlem1  29387  frrlem4  29390  frrlem5e  29395  frrlem11  29399  imagesset  29603  altopthsn  29611  mblfinlem3  30053  fnessref  30175  refssfne  30176  topjoin  30183  neifg  30189  totbndss  30273  heibor1lem  30305  unichnidl  30428  ispridl  30431  maxidlmax  30440  igenval  30458  igenidl  30460  igenmin  30461  igenval2  30463  nacsfix  30644  mzpcompact2  30685  rgspnval  31117  rgspncl  31118  rgspnmin  31120  ssrecnpr  31188  islptre  31625  bnj1286  34075  bnj1452  34108  bj-snglex  34531  lsatcmp  34728  lcvexchlem4  34762  lcvexchlem5  34763  pclvalN  35614  pclclN  35615  elpcliN  35617  docaclN  36851  dihglb2  37069  doch2val2  37091  dochocss  37093  dochexmidlem7  37193  lpolconN  37214  mapdval  37355  superficl  37752  superuncl  37753  trclub  37784  trclubg  37785
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