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

Theorem eqssd 3117
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 3115 . 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 3078
This theorem is referenced by:  uneqdifeq  3448  unissel  3754  intmin  3780  unissint  3784  int0el  3791  tz7.7  4311  reusv6OLD  4436  onint  4477  dmcosseq  4853  sofld  5028  relfld  5104  fimacnv  5509  knatar  5709  tposeq  6088  sorpssuni  6138  sorpssint  6139  onfununi  6244  tfrlem15  6294  oaass  6445  odi  6463  omass  6464  oelim2  6479  oeeui  6486  nnawordex  6521  oaabslem  6527  oaabs2  6529  omabslem  6530  omabs  6531  sucdom2  6942  fineqv  6963  dffi2  7060  fiuni  7065  dffi3  7068  ordtypelem9  7125  ordtypelem10  7126  oismo  7139  hartogslem1  7141  ixpiunwdom  7189  cantnfp1lem3  7266  oemapvali  7270  cantnf  7279  r1val1  7342  rankval3b  7382  rankunb  7406  rankuni2b  7409  rankr1id  7418  rankc2  7427  rankxplim  7433  tcrank  7438  carden2b  7484  harval2  7514  infpwfien  7573  coflim  7771  cfcof  7784  cfidm  7785  isf32lem2  7864  fin1a2lem11  7920  fin1a2lem13  7922  ttukeylem7  8026  fpwwe2  8145  winafp  8199  wuncidm  8248  wuncval2  8249  tskuni  8285  grur1  8322  distrpr  8532  prlem934  8537  ltexpri  8547  reclem4pr  8554  fzopth  10706  fzosplit  10777  fzouzsplit  10779  phimullem  12721  prmreclem5  12841  structcnvcnv  13033  imasaddfnlem  13304  imasvscafn  13313  mrcuni  13395  submrc  13397  ssceq  13547  rescabs  13554  setcepi  13764  ipopos  14107  psdmrn  14151  psssdm2  14159  dirdm  14191  gsumvallem2  14284  gsumress  14289  gsumwspan  14303  cycsubg  14480  conjnmz  14551  odf1o2  14719  gex1  14737  sylow2alem1  14763  sylow3lem3  14775  lsmidm  14808  lsmss1  14810  lsmss2  14812  lsmmod  14819  lsmdisj  14825  lsmdisj2  14826  cntzcmn  14971  prmcyg  15015  dmdprdd  15072  dprdspan  15097  dprdres  15098  dprdz  15100  subgdmdprd  15104  subgdprd  15105  dprddisj2  15109  dprd2dlem1  15111  dprd2da  15112  dmdprdsplit2lem  15115  dprdsplit  15118  ablfacrp  15136  pgpfac1lem3  15147  isdrng2  15357  issubdrg  15405  lspun  15579  lspsn  15594  lspsnneg  15598  lsp0  15601  lsslsp  15607  lmhmlsp  15641  lspextmo  15648  lsmsp  15674  lspprabs  15683  lspsnvs  15702  lspdisj  15713  lsmcv  15729  lspsnat  15732  lsppratlem6  15739  lspprat  15740  lbsextlem4  15746  lidl1el  15802  drngnidl  15813  lidldvgen  15839  fidomndrng  15880  mplbas2  16044  cnsubrg  16264  mulgrhm2  16293  znrrg  16351  ocvin  16406  ocvlsp  16408  mrccss  16426  pjfo  16447  obs2ss  16461  topsn  16505  eltg4i  16530  tgtop  16543  tgidm  16550  en2top  16555  basgen  16558  2basgen  16560  fctop  16573  cctop  16575  ppttop  16576  epttop  16578  ntrin  16630  isopn3  16635  opnnei  16689  neiuni  16691  maxlp  16710  clslp  16711  tgrest  16722  resttopon  16724  rest0  16732  restfpw  16742  restcls  16743  restntr  16744  ordtbas2  16753  ordtbas  16754  ordtrest2  16766  cmpcov2  16949  tgcmp  16960  cmpcld  16961  uncmp  16962  cmpfi  16967  2ndcsep  17017  dis2ndc  17018  restnlly  17040  dislly  17055  kgentopon  17065  kgencmp  17072  kgenidm  17074  iskgen2  17075  kgencn3  17085  ptuni2  17103  ptbasfi  17108  xkouni  17126  txcls  17131  ptclsg  17141  txdis  17158  txindis  17160  txcmplem2  17168  xkopt  17181  txcon  17215  qtopval2  17219  qtopuni  17225  qtoprest  17240  qtopomap  17241  qtopcmap  17242  kqsat  17254  kqcldsat  17256  hmeocls  17291  hmeontr  17292  hmphdis  17319  fgfil  17402  fgabs  17406  trfil1  17413  fgtr  17417  trfg  17418  uzrest  17424  ufilmax  17434  ufileu  17446  filufint  17447  ufildom1  17453  rnelfm  17480  flimfil  17496  uffclsflim  17558  alexsublem  17570  alexsubALTlem3  17575  alexsubALT  17577  ptcmplem2  17579  ptcmplem3  17580  tgpconcompeqg  17626  haustsms2  17651  tgptsmscls  17664  unirnbl  17801  iccntr  18158  pi1xfrcnv  18387  clsocv  18509  cfilfcls  18532  equivcmet  18573  pjth  18635  hlhil  18639  evthicc2  18652  ovolshft  18702  volsup  18745  dyadmbllem  18786  opnmbllem  18788  mbfconstlem  18816  itg11  18878  limciun  19076  dvidlem  19097  dvnres  19112  cpnord  19116  dvaddf  19123  dvmulf  19124  dvcmulf  19126  dvcof  19129  dvcj  19131  dvrec  19136  dvmptcmul  19145  dvcnv  19156  dvcnvre  19198  ftc1cn  19222  plyco0  19406  taylthlem1  19584  taylthlem2  19585  ulmdvlem3  19611  ulmdv  19612  pserdv  19637  wilthlem2  20139  ppisval  20173  ppisval2  20174  ppinprm  20222  chtnprm  20224  ubthlem1  21279  pjhth  21802  ococin  21817  chsupsn  21822  ssjo  21856  chabs1  21925  spansncvi  22079  mdslj1i  22729  mdslj2i  22730  atomli  22792  atcvatlem  22795  atcvat3i  22806  sumdmdlem  22828  sconpi1  22941  cvmsss2  22976  cvmliftlem15  23000  umgraex  23046  dfrtrcl2  23216  preddowncl  23364  wfi  23375  dftrpred3g  23404  trpredpo  23406  frind  23411  wfrlem10  23433  sltval2  23477  axfelem18  23531  altopthsn  23669  eqint  24125  eqintg  24126  uninqs  24204  domintrefc  24291  altprs2  24402  unint2t  24684  intfmu2  24685  islimrs4  24748  bwt2  24758  rdmob  24914  rcmob  24915  opnbnd  25409  opnregcld  25414  cldregopn  25415  fnessref  25459  comppfsc  25473  neibastop1  25474  topmeet  25479  topjoin  25480  fnemeet1  25481  fnejoin1  25483  fdc  25621  sstotbnd2  25664  isbnd2  25673  totbndbnd  25679  prdstotbnd  25684  heibor1  25700  1idl  25817  igenval2  25857  ismrcd1  25939  ismrcd2  25940  isnacs3  25951  nacsfix  25953  kercvrlsm  26347  pwssplit4  26357  frlmsslsp  26414  hbtlem5  26498  rgspnid  26543  en2other2  26548  pmtrprfv  26562  symggen  26577  bnj1136  27813  bnj1398  27850  bnj1408  27852  bnj1498  27877  lshpdisj  28081  lssats  28106  lsatcvatlem  28143  lsatcvat3  28146  lkrlsp  28196  lshpset2N  28213  lfl1dim  28215  lfl1dim2N  28216  lkrpssN  28257  paddass  28931  paddidm  28934  pmod1i  28941  pmapjat1  28946  pclbtwnN  28990  pclunN  28991  paddunN  29020  pclfinclN  29043  cdleme50rnlem  29637  dihjust  30311  dihmeetlem1N  30384  dihglblem5apreN  30385  dihmeetlem13N  30413  dochocsp  30473  dochdmj1  30484  dochnoncon  30485  dihjatb  30510  dihjat1lem  30522  lcfl9a  30599  lclkrlem2s  30619  lclkrlem2v  30622  mapdrvallem3  30740  mapdunirnN  30744  mapdin  30756  mapdlsm  30758  baerlem3lem2  30804  baerlem5alem2  30805  baerlem5blem2  30806  hdmaprnN  30961  hgmaprnN  30998  hdmaplkr  31010
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 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator