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

Theorem eqssd 3196
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 3194 . 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 1623    C_ wss 3152
This theorem is referenced by:  uneqdifeq  3542  unissel  3856  intmin  3882  unissint  3886  int0el  3893  tz7.7  4418  reusv6OLD  4545  onint  4586  dmcosseq  4946  sofld  5121  relfld  5198  fimacnv  5657  knatar  5857  tposeq  6236  sorpssuni  6286  sorpssint  6287  onfununi  6358  tfrlem15  6408  oaass  6559  odi  6577  omass  6578  oelim2  6593  oeeui  6600  nnawordex  6635  oaabslem  6641  oaabs2  6643  omabslem  6644  omabs  6645  sucdom2  7057  fineqv  7078  dffi2  7176  fiuni  7181  dffi3  7184  ordtypelem9  7241  ordtypelem10  7242  oismo  7255  hartogslem1  7257  ixpiunwdom  7305  cantnfp1lem3  7382  oemapvali  7386  cantnf  7395  r1val1  7458  rankval3b  7498  rankunb  7522  rankuni2b  7525  rankr1id  7534  rankc2  7543  rankxplim  7549  tcrank  7554  carden2b  7600  harval2  7630  infpwfien  7689  coflim  7887  cfcof  7900  cfidm  7901  isf32lem2  7980  fin1a2lem11  8036  fin1a2lem13  8038  ttukeylem7  8142  fpwwe2  8265  winafp  8319  wuncidm  8368  wuncval2  8369  tskuni  8405  grur1  8442  distrpr  8652  prlem934  8657  ltexpri  8667  reclem4pr  8674  fzopth  10828  fzosplit  10899  fzouzsplit  10901  phimullem  12847  prmreclem5  12967  structcnvcnv  13159  imasaddfnlem  13430  imasvscafn  13439  mrcuni  13523  mressmrcd  13529  submrc  13530  ssceq  13703  rescabs  13710  setcepi  13920  ipopos  14263  psdmrn  14316  psssdm2  14324  dirdm  14356  gsumvallem2  14449  gsumress  14454  gsumwspan  14468  cycsubg  14645  conjnmz  14716  odf1o2  14884  gex1  14902  sylow2alem1  14928  sylow3lem3  14940  lsmidm  14973  lsmss1  14975  lsmss2  14977  lsmmod  14984  lsmdisj  14990  lsmdisj2  14991  cntzcmn  15136  prmcyg  15180  dmdprdd  15237  dprdspan  15262  dprdres  15263  dprdz  15265  subgdmdprd  15269  subgdprd  15270  dprddisj2  15274  dprd2dlem1  15276  dprd2da  15277  dmdprdsplit2lem  15280  dprdsplit  15283  ablfacrp  15301  pgpfac1lem3  15312  isdrng2  15522  issubdrg  15570  lspun  15744  lspsn  15759  lspsnneg  15763  lsp0  15766  lsslsp  15772  lmhmlsp  15806  lspextmo  15813  lsmsp  15839  lspprabs  15848  lspsnvs  15867  lspdisj  15878  lsmcv  15894  lspsnat  15898  lsppratlem6  15905  lspprat  15906  lbsextlem4  15914  lidl1el  15970  drngnidl  15981  lidldvgen  16007  fidomndrng  16048  mplbas2  16212  cnsubrg  16432  mulgrhm2  16461  znrrg  16519  ocvin  16574  ocvlsp  16576  mrccss  16594  pjfo  16615  obs2ss  16629  topsn  16673  eltg4i  16698  tgtop  16711  tgidm  16718  en2top  16723  basgen  16726  2basgen  16728  fctop  16741  cctop  16743  ppttop  16744  epttop  16746  ntrin  16798  isopn3  16803  opnnei  16857  neiuni  16859  maxlp  16878  clslp  16879  tgrest  16890  resttopon  16892  rest0  16900  restfpw  16910  restcls  16911  restntr  16912  ordtbas2  16921  ordtbas  16922  ordtrest2  16934  cmpcov2  17117  tgcmp  17128  cmpcld  17129  uncmp  17130  cmpfi  17135  2ndcsep  17185  dis2ndc  17186  restnlly  17208  dislly  17223  kgentopon  17233  kgencmp  17240  kgenidm  17242  iskgen2  17243  kgencn3  17253  ptuni2  17271  ptbasfi  17276  xkouni  17294  txcls  17299  ptclsg  17309  txdis  17326  txindis  17328  txcmplem2  17336  xkopt  17349  txcon  17383  qtopval2  17387  qtopuni  17393  qtoprest  17408  qtopomap  17409  qtopcmap  17410  kqsat  17422  kqcldsat  17424  hmeocls  17459  hmeontr  17460  hmphdis  17487  fgfil  17570  fgabs  17574  trfil1  17581  fgtr  17585  trfg  17586  uzrest  17592  ufilmax  17602  ufileu  17614  filufint  17615  ufildom1  17621  rnelfm  17648  flimfil  17664  uffclsflim  17726  alexsublem  17738  alexsubALTlem3  17743  alexsubALT  17745  ptcmplem2  17747  ptcmplem3  17748  tgpconcompeqg  17794  haustsms2  17819  tgptsmscls  17832  unirnbl  17969  iccntr  18326  pi1xfrcnv  18555  clsocv  18677  cfilfcls  18700  equivcmet  18741  pjth  18803  hlhil  18807  evthicc2  18820  ovolshft  18870  volsup  18913  dyadmbllem  18954  opnmbllem  18956  mbfconstlem  18984  itg11  19046  limciun  19244  dvidlem  19265  dvnres  19280  cpnord  19284  dvaddf  19291  dvmulf  19292  dvcmulf  19294  dvcof  19297  dvcj  19299  dvrec  19304  dvmptcmul  19313  dvcnv  19324  dvcnvre  19366  ftc1cn  19390  plyco0  19574  taylthlem1  19752  taylthlem2  19753  ulmdvlem3  19779  ulmdv  19780  pserdv  19805  wilthlem2  20307  ppisval  20341  ppisval2  20342  ppinprm  20390  chtnprm  20392  ubthlem1  21449  pjhth  21972  ococin  21987  chsupsn  21992  ssjo  22026  chabs1  22095  spansncvi  22231  mdslj1i  22899  mdslj2i  22900  atomli  22962  atcvatlem  22965  atcvat3i  22976  sumdmdlem  22998  eqrd  23126  clduni  23289  xpinpreima2  23291  sigagenid  23511  imambfm  23567  sconpi1  23770  cvmsss2  23805  cvmliftlem15  23829  umgraex  23875  dfrtrcl2  24045  preddowncl  24196  wfi  24207  dftrpred3g  24236  trpredpo  24238  frind  24243  wfrlem10  24265  sltval2  24310  nofulllem5  24360  altopthsn  24495  eqint  24960  eqintg  24961  uninqs  25039  domintrefc  25125  altprs2  25236  unint2t  25518  intfmu2  25519  islimrs4  25582  bwt2  25592  rdmob  25748  rcmob  25749  opnbnd  26243  opnregcld  26248  cldregopn  26249  fnessref  26293  comppfsc  26307  neibastop1  26308  topmeet  26313  topjoin  26314  fnemeet1  26315  fnejoin1  26317  fdc  26455  sstotbnd2  26498  isbnd2  26507  totbndbnd  26513  prdstotbnd  26518  heibor1  26534  1idl  26651  igenval2  26691  ismrcd1  26773  ismrcd2  26774  isnacs3  26785  nacsfix  26787  kercvrlsm  27181  pwssplit4  27191  frlmsslsp  27248  hbtlem5  27332  rgspnid  27377  en2other2  27382  pmtrprfv  27396  symggen  27411  bnj1136  29027  bnj1398  29064  bnj1408  29066  bnj1498  29091  lshpdisj  29177  lssats  29202  lsatcvatlem  29239  lsatcvat3  29242  lkrlsp  29292  lshpset2N  29309  lfl1dim  29311  lfl1dim2N  29312  lkrpssN  29353  paddass  30027  paddidm  30030  pmod1i  30037  pmapjat1  30042  pclbtwnN  30086  pclunN  30087  paddunN  30116  pclfinclN  30139  cdleme50rnlem  30733  dihjust  31407  dihmeetlem1N  31480  dihglblem5apreN  31481  dihmeetlem13N  31509  dochocsp  31569  dochdmj1  31580  dochnoncon  31581  dihjatb  31606  dihjat1lem  31618  lcfl9a  31695  lclkrlem2s  31715  lclkrlem2v  31718  mapdrvallem3  31836  mapdunirnN  31840  mapdin  31852  mapdlsm  31854  baerlem3lem2  31900  baerlem5alem2  31901  baerlem5blem2  31902  hdmaprnN  32057  hgmaprnN  32094  hdmaplkr  32106
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator