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

Theorem eqssd 3197
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 3195 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3sylanbrc 648 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    = wceq 1628    C_ wss 3153
This theorem is referenced by:  uneqdifeq  3543  unissel  3857  intmin  3883  unissint  3887  int0el  3894  tz7.7  4417  reusv6OLD  4544  onint  4585  dmcosseq  4945  sofld  5120  relfld  5196  fimacnv  5618  knatar  5818  tposeq  6197  sorpssuni  6247  sorpssint  6248  onfununi  6353  tfrlem15  6403  oaass  6554  odi  6572  omass  6573  oelim2  6588  oeeui  6595  nnawordex  6630  oaabslem  6636  oaabs2  6638  omabslem  6639  omabs  6640  sucdom2  7052  fineqv  7073  dffi2  7171  fiuni  7176  dffi3  7179  ordtypelem9  7236  ordtypelem10  7237  oismo  7250  hartogslem1  7252  ixpiunwdom  7300  cantnfp1lem3  7377  oemapvali  7381  cantnf  7390  r1val1  7453  rankval3b  7493  rankunb  7517  rankuni2b  7520  rankr1id  7529  rankc2  7538  rankxplim  7544  tcrank  7549  carden2b  7595  harval2  7625  infpwfien  7684  coflim  7882  cfcof  7895  cfidm  7896  isf32lem2  7975  fin1a2lem11  8031  fin1a2lem13  8033  ttukeylem7  8137  fpwwe2  8260  winafp  8314  wuncidm  8363  wuncval2  8364  tskuni  8400  grur1  8437  distrpr  8647  prlem934  8652  ltexpri  8662  reclem4pr  8669  fzopth  10822  fzosplit  10893  fzouzsplit  10895  phimullem  12841  prmreclem5  12961  structcnvcnv  13153  imasaddfnlem  13424  imasvscafn  13433  mrcuni  13517  mressmrcd  13523  submrc  13524  ssceq  13697  rescabs  13704  setcepi  13914  ipopos  14257  psdmrn  14310  psssdm2  14318  dirdm  14350  gsumvallem2  14443  gsumress  14448  gsumwspan  14462  cycsubg  14639  conjnmz  14710  odf1o2  14878  gex1  14896  sylow2alem1  14922  sylow3lem3  14934  lsmidm  14967  lsmss1  14969  lsmss2  14971  lsmmod  14978  lsmdisj  14984  lsmdisj2  14985  cntzcmn  15130  prmcyg  15174  dmdprdd  15231  dprdspan  15256  dprdres  15257  dprdz  15259  subgdmdprd  15263  subgdprd  15264  dprddisj2  15268  dprd2dlem1  15270  dprd2da  15271  dmdprdsplit2lem  15274  dprdsplit  15277  ablfacrp  15295  pgpfac1lem3  15306  isdrng2  15516  issubdrg  15564  lspun  15738  lspsn  15753  lspsnneg  15757  lsp0  15760  lsslsp  15766  lmhmlsp  15800  lspextmo  15807  lsmsp  15833  lspprabs  15842  lspsnvs  15861  lspdisj  15872  lsmcv  15888  lspsnat  15892  lsppratlem6  15899  lspprat  15900  lbsextlem4  15908  lidl1el  15964  drngnidl  15975  lidldvgen  16001  fidomndrng  16042  mplbas2  16206  cnsubrg  16426  mulgrhm2  16455  znrrg  16513  ocvin  16568  ocvlsp  16570  mrccss  16588  pjfo  16609  obs2ss  16623  topsn  16667  eltg4i  16692  tgtop  16705  tgidm  16712  en2top  16717  basgen  16720  2basgen  16722  fctop  16735  cctop  16737  ppttop  16738  epttop  16740  ntrin  16792  isopn3  16797  opnnei  16851  neiuni  16853  maxlp  16872  clslp  16873  tgrest  16884  resttopon  16886  rest0  16894  restfpw  16904  restcls  16905  restntr  16906  ordtbas2  16915  ordtbas  16916  ordtrest2  16928  cmpcov2  17111  tgcmp  17122  cmpcld  17123  uncmp  17124  cmpfi  17129  2ndcsep  17179  dis2ndc  17180  restnlly  17202  dislly  17217  kgentopon  17227  kgencmp  17234  kgenidm  17236  iskgen2  17237  kgencn3  17247  ptuni2  17265  ptbasfi  17270  xkouni  17288  txcls  17293  ptclsg  17303  txdis  17320  txindis  17322  txcmplem2  17330  xkopt  17343  txcon  17377  qtopval2  17381  qtopuni  17387  qtoprest  17402  qtopomap  17403  qtopcmap  17404  kqsat  17416  kqcldsat  17418  hmeocls  17453  hmeontr  17454  hmphdis  17481  fgfil  17564  fgabs  17568  trfil1  17575  fgtr  17579  trfg  17580  uzrest  17586  ufilmax  17596  ufileu  17608  filufint  17609  ufildom1  17615  rnelfm  17642  flimfil  17658  uffclsflim  17720  alexsublem  17732  alexsubALTlem3  17737  alexsubALT  17739  ptcmplem2  17741  ptcmplem3  17742  tgpconcompeqg  17788  haustsms2  17813  tgptsmscls  17826  unirnbl  17963  iccntr  18320  pi1xfrcnv  18549  clsocv  18671  cfilfcls  18694  equivcmet  18735  pjth  18797  hlhil  18801  evthicc2  18814  ovolshft  18864  volsup  18907  dyadmbllem  18948  opnmbllem  18950  mbfconstlem  18978  itg11  19040  limciun  19238  dvidlem  19259  dvnres  19274  cpnord  19278  dvaddf  19285  dvmulf  19286  dvcmulf  19288  dvcof  19291  dvcj  19293  dvrec  19298  dvmptcmul  19307  dvcnv  19318  dvcnvre  19360  ftc1cn  19384  plyco0  19568  taylthlem1  19746  taylthlem2  19747  ulmdvlem3  19773  ulmdv  19774  pserdv  19799  wilthlem2  20301  ppisval  20335  ppisval2  20336  ppinprm  20384  chtnprm  20386  ubthlem1  21441  pjhth  21964  ococin  21979  chsupsn  21984  ssjo  22018  chabs1  22087  spansncvi  22223  mdslj1i  22891  mdslj2i  22892  atomli  22954  atcvatlem  22957  atcvat3i  22968  sumdmdlem  22990  sconpi1  23174  cvmsss2  23209  cvmliftlem15  23233  umgraex  23279  dfrtrcl2  23449  preddowncl  23597  wfi  23608  dftrpred3g  23637  trpredpo  23639  frind  23644  wfrlem10  23666  sltval2  23710  axfelem18  23764  altopthsn  23902  eqint  24358  eqintg  24359  uninqs  24437  domintrefc  24524  altprs2  24635  unint2t  24917  intfmu2  24918  islimrs4  24981  bwt2  24991  rdmob  25147  rcmob  25148  opnbnd  25642  opnregcld  25647  cldregopn  25648  fnessref  25692  comppfsc  25706  neibastop1  25707  topmeet  25712  topjoin  25713  fnemeet1  25714  fnejoin1  25716  fdc  25854  sstotbnd2  25897  isbnd2  25906  totbndbnd  25912  prdstotbnd  25917  heibor1  25933  1idl  26050  igenval2  26090  ismrcd1  26172  ismrcd2  26173  isnacs3  26184  nacsfix  26186  kercvrlsm  26580  pwssplit4  26590  frlmsslsp  26647  hbtlem5  26731  rgspnid  26776  en2other2  26781  pmtrprfv  26795  symggen  26810  bnj1136  28294  bnj1398  28331  bnj1408  28333  bnj1498  28358  lshpdisj  28444  lssats  28469  lsatcvatlem  28506  lsatcvat3  28509  lkrlsp  28559  lshpset2N  28576  lfl1dim  28578  lfl1dim2N  28579  lkrpssN  28620  paddass  29294  paddidm  29297  pmod1i  29304  pmapjat1  29309  pclbtwnN  29353  pclunN  29354  paddunN  29383  pclfinclN  29406  cdleme50rnlem  30000  dihjust  30674  dihmeetlem1N  30747  dihglblem5apreN  30748  dihmeetlem13N  30776  dochocsp  30836  dochdmj1  30847  dochnoncon  30848  dihjatb  30873  dihjat1lem  30885  lcfl9a  30962  lclkrlem2s  30982  lclkrlem2v  30985  mapdrvallem3  31103  mapdunirnN  31107  mapdin  31119  mapdlsm  31121  baerlem3lem2  31167  baerlem5alem2  31168  baerlem5blem2  31169  hdmaprnN  31324  hgmaprnN  31361  hdmaplkr  31373
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1538  ax-5 1549  ax-17 1608  ax-9 1641  ax-8 1648  ax-6 1707  ax-7 1712  ax-11 1719  ax-12 1869  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1534  df-nf 1537  df-sb 1636  df-clab 2271  df-cleq 2277  df-clel 2280  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator