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

Theorem eqssd 3171
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 3169 . 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 1619    C_ wss 3127
This theorem is referenced by:  uneqdifeq  3517  unissel  3830  intmin  3856  unissint  3860  int0el  3867  tz7.7  4390  reusv6OLD  4517  onint  4558  dmcosseq  4934  sofld  5109  relfld  5185  fimacnv  5591  knatar  5791  tposeq  6170  sorpssuni  6220  sorpssint  6221  onfununi  6326  tfrlem15  6376  oaass  6527  odi  6545  omass  6546  oelim2  6561  oeeui  6568  nnawordex  6603  oaabslem  6609  oaabs2  6611  omabslem  6612  omabs  6613  sucdom2  7025  fineqv  7046  dffi2  7144  fiuni  7149  dffi3  7152  ordtypelem9  7209  ordtypelem10  7210  oismo  7223  hartogslem1  7225  ixpiunwdom  7273  cantnfp1lem3  7350  oemapvali  7354  cantnf  7363  r1val1  7426  rankval3b  7466  rankunb  7490  rankuni2b  7493  rankr1id  7502  rankc2  7511  rankxplim  7517  tcrank  7522  carden2b  7568  harval2  7598  infpwfien  7657  coflim  7855  cfcof  7868  cfidm  7869  isf32lem2  7948  fin1a2lem11  8004  fin1a2lem13  8006  ttukeylem7  8110  fpwwe2  8233  winafp  8287  wuncidm  8336  wuncval2  8337  tskuni  8373  grur1  8410  distrpr  8620  prlem934  8625  ltexpri  8635  reclem4pr  8642  fzopth  10794  fzosplit  10865  fzouzsplit  10867  phimullem  12809  prmreclem5  12929  structcnvcnv  13121  imasaddfnlem  13392  imasvscafn  13401  mrcuni  13485  mressmrcd  13491  submrc  13492  ssceq  13665  rescabs  13672  setcepi  13882  ipopos  14225  psdmrn  14278  psssdm2  14286  dirdm  14318  gsumvallem2  14411  gsumress  14416  gsumwspan  14430  cycsubg  14607  conjnmz  14678  odf1o2  14846  gex1  14864  sylow2alem1  14890  sylow3lem3  14902  lsmidm  14935  lsmss1  14937  lsmss2  14939  lsmmod  14946  lsmdisj  14952  lsmdisj2  14953  cntzcmn  15098  prmcyg  15142  dmdprdd  15199  dprdspan  15224  dprdres  15225  dprdz  15227  subgdmdprd  15231  subgdprd  15232  dprddisj2  15236  dprd2dlem1  15238  dprd2da  15239  dmdprdsplit2lem  15242  dprdsplit  15245  ablfacrp  15263  pgpfac1lem3  15274  isdrng2  15484  issubdrg  15532  lspun  15706  lspsn  15721  lspsnneg  15725  lsp0  15728  lsslsp  15734  lmhmlsp  15768  lspextmo  15775  lsmsp  15801  lspprabs  15810  lspsnvs  15829  lspdisj  15840  lsmcv  15856  lspsnat  15860  lsppratlem6  15867  lspprat  15868  lbsextlem4  15876  lidl1el  15932  drngnidl  15943  lidldvgen  15969  fidomndrng  16010  mplbas2  16174  cnsubrg  16394  mulgrhm2  16423  znrrg  16481  ocvin  16536  ocvlsp  16538  mrccss  16556  pjfo  16577  obs2ss  16591  topsn  16635  eltg4i  16660  tgtop  16673  tgidm  16680  en2top  16685  basgen  16688  2basgen  16690  fctop  16703  cctop  16705  ppttop  16706  epttop  16708  ntrin  16760  isopn3  16765  opnnei  16819  neiuni  16821  maxlp  16840  clslp  16841  tgrest  16852  resttopon  16854  rest0  16862  restfpw  16872  restcls  16873  restntr  16874  ordtbas2  16883  ordtbas  16884  ordtrest2  16896  cmpcov2  17079  tgcmp  17090  cmpcld  17091  uncmp  17092  cmpfi  17097  2ndcsep  17147  dis2ndc  17148  restnlly  17170  dislly  17185  kgentopon  17195  kgencmp  17202  kgenidm  17204  iskgen2  17205  kgencn3  17215  ptuni2  17233  ptbasfi  17238  xkouni  17256  txcls  17261  ptclsg  17271  txdis  17288  txindis  17290  txcmplem2  17298  xkopt  17311  txcon  17345  qtopval2  17349  qtopuni  17355  qtoprest  17370  qtopomap  17371  qtopcmap  17372  kqsat  17384  kqcldsat  17386  hmeocls  17421  hmeontr  17422  hmphdis  17449  fgfil  17532  fgabs  17536  trfil1  17543  fgtr  17547  trfg  17548  uzrest  17554  ufilmax  17564  ufileu  17576  filufint  17577  ufildom1  17583  rnelfm  17610  flimfil  17626  uffclsflim  17688  alexsublem  17700  alexsubALTlem3  17705  alexsubALT  17707  ptcmplem2  17709  ptcmplem3  17710  tgpconcompeqg  17756  haustsms2  17781  tgptsmscls  17794  unirnbl  17931  iccntr  18288  pi1xfrcnv  18517  clsocv  18639  cfilfcls  18662  equivcmet  18703  pjth  18765  hlhil  18769  evthicc2  18782  ovolshft  18832  volsup  18875  dyadmbllem  18916  opnmbllem  18918  mbfconstlem  18946  itg11  19008  limciun  19206  dvidlem  19227  dvnres  19242  cpnord  19246  dvaddf  19253  dvmulf  19254  dvcmulf  19256  dvcof  19259  dvcj  19261  dvrec  19266  dvmptcmul  19275  dvcnv  19286  dvcnvre  19328  ftc1cn  19352  plyco0  19536  taylthlem1  19714  taylthlem2  19715  ulmdvlem3  19741  ulmdv  19742  pserdv  19767  wilthlem2  20269  ppisval  20303  ppisval2  20304  ppinprm  20352  chtnprm  20354  ubthlem1  21409  pjhth  21932  ococin  21947  chsupsn  21952  ssjo  21986  chabs1  22055  spansncvi  22191  mdslj1i  22859  mdslj2i  22860  atomli  22922  atcvatlem  22925  atcvat3i  22936  sumdmdlem  22958  sconpi1  23142  cvmsss2  23177  cvmliftlem15  23201  umgraex  23247  dfrtrcl2  23417  preddowncl  23565  wfi  23576  dftrpred3g  23605  trpredpo  23607  frind  23612  wfrlem10  23634  sltval2  23678  axfelem18  23732  altopthsn  23870  eqint  24326  eqintg  24327  uninqs  24405  domintrefc  24492  altprs2  24603  unint2t  24885  intfmu2  24886  islimrs4  24949  bwt2  24959  rdmob  25115  rcmob  25116  opnbnd  25610  opnregcld  25615  cldregopn  25616  fnessref  25660  comppfsc  25674  neibastop1  25675  topmeet  25680  topjoin  25681  fnemeet1  25682  fnejoin1  25684  fdc  25822  sstotbnd2  25865  isbnd2  25874  totbndbnd  25880  prdstotbnd  25885  heibor1  25901  1idl  26018  igenval2  26058  ismrcd1  26140  ismrcd2  26141  isnacs3  26152  nacsfix  26154  kercvrlsm  26548  pwssplit4  26558  frlmsslsp  26615  hbtlem5  26699  rgspnid  26744  en2other2  26749  pmtrprfv  26763  symggen  26778  bnj1136  28076  bnj1398  28113  bnj1408  28115  bnj1498  28140  lshpdisj  28344  lssats  28369  lsatcvatlem  28406  lsatcvat3  28409  lkrlsp  28459  lshpset2N  28476  lfl1dim  28478  lfl1dim2N  28479  lkrpssN  28520  paddass  29194  paddidm  29197  pmod1i  29204  pmapjat1  29209  pclbtwnN  29253  pclunN  29254  paddunN  29283  pclfinclN  29306  cdleme50rnlem  29900  dihjust  30574  dihmeetlem1N  30647  dihglblem5apreN  30648  dihmeetlem13N  30676  dochocsp  30736  dochdmj1  30747  dochnoncon  30748  dihjatb  30773  dihjat1lem  30785  lcfl9a  30862  lclkrlem2s  30882  lclkrlem2v  30885  mapdrvallem3  31003  mapdunirnN  31007  mapdin  31019  mapdlsm  31021  baerlem3lem2  31067  baerlem5alem2  31068  baerlem5blem2  31069  hdmaprnN  31224  hgmaprnN  31261  hdmaplkr  31273
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-in 3134  df-ss 3141
  Copyright terms: Public domain W3C validator