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

Theorem eqssd 3520
Description: Equality deduction from two subclass relationships. Compare Theorem 4 of [Suppes] p. 22. (Contributed by NM, 27-Jun-2004.)
Hypotheses
Ref Expression
eqssd.1
eqssd.2
Assertion
Ref Expression
eqssd

Proof of Theorem eqssd
StepHypRef Expression
1 eqssd.1 . 2
2 eqssd.2 . 2
3 eqss 3518 . 2
41, 2, 3sylanbrc 664 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475
This theorem is referenced by:  eqrd  3521  uneqdifeq  3916  unissel  4280  intmin  4306  unissint  4311  int0el  4318  reusv6OLD  4663  tz7.7  4909  dmcosseq  5269  sofld  5460  relfld  5538  fimacnv  6019  knatar  6253  sorpssuni  6589  sorpssint  6590  onint  6630  fo2ndf  6907  suppimacnv  6929  tposeq  6976  onfununi  7031  tfrlem15  7080  oaass  7229  odi  7247  omass  7248  oelim2  7263  oeeui  7270  nnawordex  7305  oaabslem  7311  oaabs2  7313  omabslem  7314  omabs  7315  uniinqs  7410  sucdom2  7734  fineqv  7755  dffi2  7903  fiuni  7908  dffi3  7911  ordtypelem9  7972  ordtypelem10  7973  oismo  7986  hartogslem1  7988  ixpiunwdom  8038  cantnfp1lem3  8120  oemapvali  8124  cantnf  8133  cantnfp1lem3OLD  8146  cantnfOLD  8155  r1val1  8225  rankval3b  8265  rankunb  8289  rankuni2b  8292  rankr1id  8301  rankc2  8310  rankxplim  8318  tcrank  8323  carden2b  8369  harval2  8399  en2other2  8408  infpwfien  8464  coflim  8662  cfcof  8675  cfidm  8676  isf32lem2  8755  fin1a2lem11  8811  fin1a2lem13  8813  ttukeylem7  8916  fpwwe2  9042  winafp  9096  wuncidm  9145  wuncval2  9146  tskuni  9182  grur1  9219  distrpr  9427  prlem934  9432  ltexpri  9442  reclem4pr  9449  fzopth  11749  fzosplit  11858  fzouzsplit  11860  ccatrn  12606  phimullem  14309  prmreclem5  14438  structcnvcnv  14643  imasaddfnlem  14925  imasvscafn  14934  mrcuni  15018  mressmrcd  15024  submrc  15025  ssceq  15195  rescabs  15202  setcepi  15415  clatl  15746  ipopos  15790  psdmrn  15837  psssdm2  15845  dirdm  15864  gsumress  15903  gsumvallem2  16003  gsumwspan  16014  cycsubg  16229  conjnmz  16300  pmtrprfv  16478  symggen  16495  odf1o2  16593  gex1  16611  sylow2alem1  16637  sylow3lem3  16649  lsmidm  16682  lsmss1  16684  lsmss2  16686  lsmmod  16693  lsmdisj  16699  lsmdisj2  16700  cntzcmn  16848  prmcyg  16896  dmdprdd  17030  dprdspan  17074  dprdres  17075  dprdz  17077  subgdmdprd  17081  subgdprd  17082  dprddisj2  17087  dprddisj2OLD  17088  dprd2dlem1  17090  dprd2da  17091  dmdprdsplit2lem  17094  dprdsplit  17097  ablfacrp  17117  pgpfac1lem3  17128  kerf1hrm  17392  isdrng2  17406  issubdrg  17454  lspun  17633  lspsn  17648  lspsnneg  17652  lsp0  17655  lsslsp  17661  lmhmlsp  17695  lspextmo  17702  lsmsp  17732  lspprabs  17741  lspsnvs  17760  lspdisj  17771  lsmcv  17787  lspsnat  17791  lsppratlem6  17798  lspprat  17799  lbsextlem4  17807  lidl1el  17866  drngnidl  17877  lidldvgen  17903  fidomndrng  17956  mplbas2  18134  mplbas2OLD  18135  cnsubrg  18478  mulgrhm2  18533  mulgrhm2OLD  18536  znrrg  18604  ocvin  18705  ocvlsp  18707  mrccss  18725  pjfo  18746  obs2ss  18760  frlmsslsp  18829  frlmsslspOLD  18830  topsn  19436  eltg4i  19461  unitg  19468  tgtop  19475  tgidm  19482  en2top  19487  basgen  19490  2basgen  19492  fctop  19505  cctop  19507  ppttop  19508  epttop  19510  ntrin  19562  isopn3  19567  opnnei  19621  neiuni  19623  maxlp  19648  clslp  19649  tgrest  19660  resttopon  19662  rest0  19670  restfpw  19680  restcls  19682  restntr  19683  ordtbas2  19692  ordtbas  19693  ordtrest2  19705  cmpcov2  19890  tgcmp  19901  cmpcld  19902  uncmp  19903  cmpfi  19908  bwthOLD  19911  2ndcsep  19960  dis2ndc  19961  restnlly  19983  dislly  19998  comppfsc  20033  kgentopon  20039  kgencmp  20046  kgenidm  20048  iskgen2  20049  kgencn3  20059  ptuni2  20077  ptbasfi  20082  xkouni  20100  txcls  20105  ptclsg  20116  txdis  20133  txindis  20135  txcmplem2  20143  xkopt  20156  txcon  20190  qtopval2  20197  qtopuni  20203  qtoprest  20218  qtopomap  20219  qtopcmap  20220  kqsat  20232  kqcldsat  20234  hmeocls  20269  hmeontr  20270  hmphdis  20297  fgfil  20376  fgabs  20380  trfil1  20387  fgtr  20391  trfg  20392  uzrest  20398  ufilmax  20408  ufileu  20420  filufint  20421  ufildom1  20427  rnelfm  20454  flimfil  20470  uffclsflim  20532  alexsublem  20544  alexsubALTlem3  20549  alexsubALT  20551  ptcmplem2  20553  ptcmplem3  20554  tgpconcompeqg  20610  haustsms2  20635  tgptsmscls  20652  ust0  20722  ustbas2  20728  restutopopn  20741  unirnblps  20922  unirnbl  20923  iccntr  21326  pi1xfrcnv  21557  clsocv  21690  cfilfcls  21713  equivcmet  21754  pjth  21854  hlhil  21858  evthicc2  21872  ovolshft  21922  volsup  21966  dyadmbllem  22008  opnmbllem  22010  mbfconstlem  22036  itg11  22098  limciun  22298  dvidlem  22319  dvnres  22334  cpnord  22338  dvaddf  22345  dvmulf  22346  dvcmulf  22348  dvcof  22351  dvcj  22353  dvrec  22358  dvmptcmul  22367  dvcnv  22378  dvcnvre  22420  ftc1cn  22444  plyco0  22589  taylthlem1  22768  taylthlem2  22769  ulmdvlem3  22797  ulmdv  22798  pserdv  22824  wilthlem2  23343  ppisval  23377  ppisval2  23378  ppinprm  23426  chtnprm  23428  umgraex  24323  ubthlem1  25786  pjhth  26311  ococin  26326  chsupsn  26331  ssjo  26365  chabs1  26434  spansncvi  26570  mdslj1i  27238  mdslj2i  27239  atomli  27301  atcvatlem  27304  atcvat3i  27315  sumdmdlem  27337  reff  27842  cmpcref  27853  xpinpreima2  27889  ordtrest2NEW  27905  sigagenid  28151  imambfm  28233  dya2iocuni  28254  sconpi1  28684  cvmsss2  28719  cvmliftlem15  28743  dfrtrcl2  29071  preddowncl  29276  wfi  29287  dftrpred3g  29316  trpredpo  29318  frind  29323  wfrlem10  29352  sltval2  29416  nofulllem5  29466  altopthsn  29611  opnmbllem0  30050  ftc1cnnc  30089  opnbnd  30143  opnregcld  30148  cldregopn  30149  fnessref  30175  neibastop1  30177  topmeet  30182  topjoin  30183  fnemeet1  30184  fnejoin1  30186  fdc  30238  sstotbnd2  30270  isbnd2  30279  totbndbnd  30285  prdstotbnd  30290  heibor1  30306  1idl  30423  igenval2  30463  ismrcd1  30630  ismrcd2  30631  isnacs3  30642  nacsfix  30644  kercvrlsm  31029  pwssplit4  31035  hbtlem5  31077  rgspnid  31121  iocinico  31179  nzin  31223  icoiccdif  31564  lptioo2  31637  lptioo1  31638  fourierdlem79  31968  fzoopth  32340  lspeqlco  33040  bnj1136  34053  bnj1398  34090  bnj1408  34092  bnj1498  34117  lshpdisj  34712  lssats  34737  lsatcvat3  34777  lkrlsp  34827  lshpset2N  34844  lfl1dim  34846  lfl1dim2N  34847  lkrpssN  34888  paddass  35562  paddidm  35565  pmod1i  35572  pmapjat1  35577  pclbtwnN  35621  pclunN  35622  paddunN  35651  pclfinclN  35674  cdleme50rnlem  36270  dihjust  36944  dihmeetlem1N  37017  dihglblem5apreN  37018  dihmeetlem13N  37046  dochocsp  37106  dochdmj1  37117  dochnoncon  37118  dihjatb  37143  dihjat1lem  37155  lcfl9a  37232  lclkrlem2s  37252  lclkrlem2v  37255  mapdrvallem3  37373  mapdunirnN  37377  mapdin  37389  mapdlsm  37391  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439  hdmaprnN  37594  hgmaprnN  37631  hdmaplkr  37643
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