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

Theorem sseq2d 3531
Description: An equality deduction for the subclass relationship. (Contributed by NM, 14-Aug-1994.)
Hypothesis
Ref Expression
sseq1d.1
Assertion
Ref Expression
sseq2d

Proof of Theorem sseq2d
StepHypRef Expression
1 sseq1d.1 . 2
2 sseq2 3525 . 2
31, 2syl 16 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  <->wb 184  =wceq 1395  C_wss 3475
This theorem is referenced by:  sseq12d  3532  sseqtrd  3539  sbcrel  5094  funimass2  5667  fnco  5694  fnssresb  5698  fnimaeq0  5707  foimacnv  5838  fvelimab  5929  ssimaexg  5939  knatar  6253  onfununi  7031  oaordi  7214  oawordeulem  7222  oaass  7229  odi  7247  omass  7248  oen0  7254  oelim2  7263  nnaordi  7286  nnawordex  7305  pssnn  7758  fissuni  7845  dffi3  7911  cantnfle  8111  cantnflem1  8129  cantnfleOLD  8141  cantnflem1OLD  8152  trcl  8180  r1sdom  8213  iscard2  8378  alephordi  8476  alephgeom  8484  cardaleph  8491  cardalephex  8492  ackbij2lem4  8643  cflm  8651  cfslbn  8668  cofsmo  8670  cfsmolem  8671  cfcoflem  8673  coftr  8674  alephsing  8677  fin23lem28  8741  fin23lem30  8743  fin23lem33  8746  fin1a2lem9  8809  axdc3lem2  8852  ttukeylem5  8914  fpwwe2lem5  9033  pwfseqlem4a  9060  pwfseqlem4  9061  wunex2  9137  inar1  9174  sstskm  9241  fsuppmapnn0fiubex  12098  swrdnd  12657  swrd0  12658  repswswrd  12756  summolem2  13538  summo  13539  zsum  13540  sumz  13544  sumss  13546  fsumcvg3  13551  prodmolem2  13742  prodmo  13743  zprod  13744  prod1  13751  vdwlem1  14499  vdwlem12  14510  vdwlem13  14511  ramub2  14532  rami  14533  ramz2  14542  prdsval  14852  pwsle  14889  mrcuni  15018  gsumpropd  15899  gsumpropd2lem  15900  gsumress  15903  eqgfval  16249  sscntz  16364  resscntz  16369  lsmlub  16683  efgrelexlemb  16768  efgcpbllemb  16773  gsumval3a  16905  gsumval3aOLD  16906  gsumzaddlem  16934  gsumzoppg  16967  dmdprd  17029  dprdcntz  17041  subgdmdprd  17081  subrgpropd  17463  islss  17581  lsslss  17607  lsspropd  17663  lsmelpr  17737  lbspropd  17745  ltbval  18136  opsrval  18139  lsslinds  18866  isbasisg  19448  tgval  19456  tgss3  19488  restbas  19659  tgrest  19660  restcld  19673  restopn2  19678  restntr  19683  cnpnei  19765  cncls2  19774  perfcls  19866  cmpsublem  19899  cmpsub  19900  cmpcld  19902  uncmp  19903  hauscmplem  19906  cmpfi  19908  nconsubb  19924  clscon  19931  hausllycmp  19995  1stckgenlem  20054  txbas  20068  ptbasfi  20082  txcnpi  20109  ptcnp  20123  txcmplem1  20142  txcmplem2  20143  xkococnlem  20160  qtopcld  20214  fbasssin  20337  fbssint  20339  fbun  20341  fbasrn  20385  filufint  20421  ufinffr  20430  ufildr  20432  ustval  20705  trust  20732  elmopn  20945  neibl  21004  cfilucfilOLD  21072  cfilucfil  21073  icccmplem1  21327  icccmplem2  21328  bndth  21458  isphtpc  21494  metcld  21744  bcthlem1  21763  bcth  21768  ovolfioo  21879  ovolficc  21880  elovolmr  21887  ovoliunlem3  21915  ovolicc2  21933  volsuplem  21965  dyadmax  22007  dyadmbllem  22008  dyadmbl  22009  isfrgra  24990  sspval  25636  ubth  25789  orthin  26364  chssoc  26414  chsscon3  26418  chsscon1  26419  h1datom  26500  pjoml6i  26507  osum  26563  spansncv  26571  pjcjt2  26610  pjopyth  26638  hstel2  27138  hstle  27149  stj  27154  dmdbr5  27227  mdslmd1lem1  27244  atord  27307  chirredlem4  27312  atcvat4i  27316  mdsymlem2  27323  mdsymlem3  27324  mdsymlem8  27329  ssnnssfz  27597  tpr2rico  27894  ordtrestNEW  27903  sigaval  28110  issiga  28111  issgon  28123  oms0  28266  kur14  28660  cvmliftlem15  28743  mclsrcl  28921  mclsval  28923  ghomfo  29031  rtrclreclem.refl  29067  rtrclreclem.subset  29068  trpredtr  29313  dftrpred3g  29316  wfrlem9  29351  wfrlem12  29354  frrlem5e  29395  nofulllem1  29462  nofulllem2  29463  mblfinlem2  30052  ivthALT  30153  isfne  30157  topfne  30172  neibastop3  30180  tailfb  30195  filnetlem1  30196  filnetlem4  30199  sstotbnd2  30270  sstotbnd  30271  sstotbnd3  30272  ssbnd  30284  cntotbnd  30292  cnpwstotbnd  30293  ismtyres  30304  heibor1lem  30305  heiborlem1  30307  heiborlem6  30312  heiborlem8  30314  exidreslem  30339  scottexf  30576  scott0f  30577  ismrc  30633  incssnn0  30643  nacsfix  30644  hbt  31079  stoweidlem50  31832  stoweidlem57  31839  fourierdlem20  31909  fourierdlem50  31939  fourierdlem64  31953  fourierdlem86  31975  fourierdlem103  31992  fourierdlem104  31993  edgssv2ALT  32401  edgssv2  32402  ssnn0ssfz  32938  lincfsuppcl  33014  lshpcmp  34713  lsmsat  34733  lsmsatcv  34735  lfl1dim  34846  lfl1dim2N  34847  lkrss2N  34894  psubspset  35468  paddss  35569  psubclsetN  35660  dilfsetN  35877  dilsetN  35878  diaglbN  36782  dibglbN  36893  dihlspsnat  37060  dihglb2  37069  dochffval  37076  dochfval  37077  dochvalr  37084  dochord2N  37098  dochsncom  37109  dihjat1lem  37155  dvh4dimat  37165  dvh3dimatN  37166  dvh2dimatN  37167  dochexmidlem1  37187  lpolsetN  37209  lpolconN  37214  hdmaplkr  37643  hdmapoc  37661  hlhillcs  37688
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