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

Theorem eqssd 3209
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  |-  ( ph  ->  A  C_  B )
eqssd.2  |-  ( ph  ->  B  C_  A )
Assertion
Ref Expression
eqssd  |-  ( ph  ->  A  =  B )

Proof of Theorem eqssd
StepHypRef Expression
1 eqssd.1 . 2  |-  ( ph  ->  A  C_  B )
2 eqssd.2 . 2  |-  ( ph  ->  B  C_  A )
3 eqss 3207 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3sylanbrc 645 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165
This theorem is referenced by:  uneqdifeq  3555  unissel  3872  intmin  3898  unissint  3902  int0el  3909  tz7.7  4434  reusv6OLD  4561  onint  4602  dmcosseq  4962  sofld  5137  relfld  5214  fimacnv  5673  knatar  5873  tposeq  6252  sorpssuni  6302  sorpssint  6303  onfununi  6374  tfrlem15  6424  oaass  6575  odi  6593  omass  6594  oelim2  6609  oeeui  6616  nnawordex  6651  oaabslem  6657  oaabs2  6659  omabslem  6660  omabs  6661  sucdom2  7073  fineqv  7094  dffi2  7192  fiuni  7197  dffi3  7200  ordtypelem9  7257  ordtypelem10  7258  oismo  7271  hartogslem1  7273  ixpiunwdom  7321  cantnfp1lem3  7398  oemapvali  7402  cantnf  7411  r1val1  7474  rankval3b  7514  rankunb  7538  rankuni2b  7541  rankr1id  7550  rankc2  7559  rankxplim  7565  tcrank  7570  carden2b  7616  harval2  7646  infpwfien  7705  coflim  7903  cfcof  7916  cfidm  7917  isf32lem2  7996  fin1a2lem11  8052  fin1a2lem13  8054  ttukeylem7  8158  fpwwe2  8281  winafp  8335  wuncidm  8384  wuncval2  8385  tskuni  8421  grur1  8458  distrpr  8668  prlem934  8673  ltexpri  8683  reclem4pr  8690  fzopth  10844  fzosplit  10915  fzouzsplit  10917  phimullem  12863  prmreclem5  12983  structcnvcnv  13175  imasaddfnlem  13446  imasvscafn  13455  mrcuni  13539  mressmrcd  13545  submrc  13546  ssceq  13719  rescabs  13726  setcepi  13936  ipopos  14279  psdmrn  14332  psssdm2  14340  dirdm  14372  gsumvallem2  14465  gsumress  14470  gsumwspan  14484  cycsubg  14661  conjnmz  14732  odf1o2  14900  gex1  14918  sylow2alem1  14944  sylow3lem3  14956  lsmidm  14989  lsmss1  14991  lsmss2  14993  lsmmod  15000  lsmdisj  15006  lsmdisj2  15007  cntzcmn  15152  prmcyg  15196  dmdprdd  15253  dprdspan  15278  dprdres  15279  dprdz  15281  subgdmdprd  15285  subgdprd  15286  dprddisj2  15290  dprd2dlem1  15292  dprd2da  15293  dmdprdsplit2lem  15296  dprdsplit  15299  ablfacrp  15317  pgpfac1lem3  15328  isdrng2  15538  issubdrg  15586  lspun  15760  lspsn  15775  lspsnneg  15779  lsp0  15782  lsslsp  15788  lmhmlsp  15822  lspextmo  15829  lsmsp  15855  lspprabs  15864  lspsnvs  15883  lspdisj  15894  lsmcv  15910  lspsnat  15914  lsppratlem6  15921  lspprat  15922  lbsextlem4  15930  lidl1el  15986  drngnidl  15997  lidldvgen  16023  fidomndrng  16064  mplbas2  16228  cnsubrg  16448  mulgrhm2  16477  znrrg  16535  ocvin  16590  ocvlsp  16592  mrccss  16610  pjfo  16631  obs2ss  16645  topsn  16689  eltg4i  16714  tgtop  16727  tgidm  16734  en2top  16739  basgen  16742  2basgen  16744  fctop  16757  cctop  16759  ppttop  16760  epttop  16762  ntrin  16814  isopn3  16819  opnnei  16873  neiuni  16875  maxlp  16894  clslp  16895  tgrest  16906  resttopon  16908  rest0  16916  restfpw  16926  restcls  16927  restntr  16928  ordtbas2  16937  ordtbas  16938  ordtrest2  16950  cmpcov2  17133  tgcmp  17144  cmpcld  17145  uncmp  17146  cmpfi  17151  2ndcsep  17201  dis2ndc  17202  restnlly  17224  dislly  17239  kgentopon  17249  kgencmp  17256  kgenidm  17258  iskgen2  17259  kgencn3  17269  ptuni2  17287  ptbasfi  17292  xkouni  17310  txcls  17315  ptclsg  17325  txdis  17342  txindis  17344  txcmplem2  17352  xkopt  17365  txcon  17399  qtopval2  17403  qtopuni  17409  qtoprest  17424  qtopomap  17425  qtopcmap  17426  kqsat  17438  kqcldsat  17440  hmeocls  17475  hmeontr  17476  hmphdis  17503  fgfil  17586  fgabs  17590  trfil1  17597  fgtr  17601  trfg  17602  uzrest  17608  ufilmax  17618  ufileu  17630  filufint  17631  ufildom1  17637  rnelfm  17664  flimfil  17680  uffclsflim  17742  alexsublem  17754  alexsubALTlem3  17759  alexsubALT  17761  ptcmplem2  17763  ptcmplem3  17764  tgpconcompeqg  17810  haustsms2  17835  tgptsmscls  17848  unirnbl  17985  iccntr  18342  pi1xfrcnv  18571  clsocv  18693  cfilfcls  18716  equivcmet  18757  pjth  18819  hlhil  18823  evthicc2  18836  ovolshft  18886  volsup  18929  dyadmbllem  18970  opnmbllem  18972  mbfconstlem  19000  itg11  19062  limciun  19260  dvidlem  19281  dvnres  19296  cpnord  19300  dvaddf  19307  dvmulf  19308  dvcmulf  19310  dvcof  19313  dvcj  19315  dvrec  19320  dvmptcmul  19329  dvcnv  19340  dvcnvre  19382  ftc1cn  19406  plyco0  19590  taylthlem1  19768  taylthlem2  19769  ulmdvlem3  19795  ulmdv  19796  pserdv  19821  wilthlem2  20323  ppisval  20357  ppisval2  20358  ppinprm  20406  chtnprm  20408  ubthlem1  21465  pjhth  21988  ococin  22003  chsupsn  22008  ssjo  22042  chabs1  22111  spansncvi  22247  mdslj1i  22915  mdslj2i  22916  atomli  22978  atcvatlem  22981  atcvat3i  22992  sumdmdlem  23014  eqrd  23142  clduni  23304  xpinpreima2  23306  sigagenid  23526  imambfm  23582  sconpi1  23785  cvmsss2  23820  cvmliftlem15  23844  umgraex  23890  dfrtrcl2  24060  preddowncl  24267  wfi  24278  dftrpred3g  24307  trpredpo  24309  frind  24314  wfrlem10  24336  sltval2  24381  nofulllem5  24431  altopthsn  24567  ftc1cnnc  25025  eqint  25063  eqintg  25064  uninqs  25142  domintrefc  25228  altprs2  25339  unint2t  25621  intfmu2  25622  islimrs4  25685  bwt2  25695  rdmob  25851  rcmob  25852  opnbnd  26346  opnregcld  26351  cldregopn  26352  fnessref  26396  comppfsc  26410  neibastop1  26411  topmeet  26416  topjoin  26417  fnemeet1  26418  fnejoin1  26420  fdc  26558  sstotbnd2  26601  isbnd2  26610  totbndbnd  26616  prdstotbnd  26621  heibor1  26637  1idl  26754  igenval2  26794  ismrcd1  26876  ismrcd2  26877  isnacs3  26888  nacsfix  26890  kercvrlsm  27284  pwssplit4  27294  frlmsslsp  27351  hbtlem5  27435  rgspnid  27480  en2other2  27485  pmtrprfv  27499  symggen  27514  bnj1136  29343  bnj1398  29380  bnj1408  29382  bnj1498  29407  lshpdisj  29799  lssats  29824  lsatcvatlem  29861  lsatcvat3  29864  lkrlsp  29914  lshpset2N  29931  lfl1dim  29933  lfl1dim2N  29934  lkrpssN  29975  paddass  30649  paddidm  30652  pmod1i  30659  pmapjat1  30664  pclbtwnN  30708  pclunN  30709  paddunN  30738  pclfinclN  30761  cdleme50rnlem  31355  dihjust  32029  dihmeetlem1N  32102  dihglblem5apreN  32103  dihmeetlem13N  32131  dochocsp  32191  dochdmj1  32202  dochnoncon  32203  dihjatb  32228  dihjat1lem  32240  lcfl9a  32317  lclkrlem2s  32337  lclkrlem2v  32340  mapdrvallem3  32458  mapdunirnN  32462  mapdin  32474  mapdlsm  32476  baerlem3lem2  32522  baerlem5alem2  32523  baerlem5blem2  32524  hdmaprnN  32679  hgmaprnN  32716  hdmaplkr  32728
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator