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

Theorem eqssd 3506
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 3504 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3sylanbrc 664 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  eqrd  3507  uneqdifeq  3902  unissel  4265  intmin  4291  unissint  4296  int0el  4303  reusv6OLD  4648  tz7.7  4894  dmcosseq  5254  sofld  5445  relfld  5523  fimacnv  6004  knatar  6238  sorpssuni  6574  sorpssint  6575  onint  6615  fo2ndf  6892  suppimacnv  6914  tposeq  6959  onfununi  7014  tfrlem15  7063  oaass  7212  odi  7230  omass  7231  oelim2  7246  oeeui  7253  nnawordex  7288  oaabslem  7294  oaabs2  7296  omabslem  7297  omabs  7298  uniinqs  7393  sucdom2  7716  fineqv  7737  dffi2  7885  fiuni  7890  dffi3  7893  ordtypelem9  7954  ordtypelem10  7955  oismo  7968  hartogslem1  7970  ixpiunwdom  8020  cantnfp1lem3  8102  oemapvali  8106  cantnf  8115  cantnfp1lem3OLD  8128  cantnfOLD  8137  r1val1  8207  rankval3b  8247  rankunb  8271  rankuni2b  8274  rankr1id  8283  rankc2  8292  rankxplim  8300  tcrank  8305  carden2b  8351  harval2  8381  en2other2  8390  infpwfien  8446  coflim  8644  cfcof  8657  cfidm  8658  isf32lem2  8737  fin1a2lem11  8793  fin1a2lem13  8795  ttukeylem7  8898  fpwwe2  9024  winafp  9078  wuncidm  9127  wuncval2  9128  tskuni  9164  grur1  9201  distrpr  9409  prlem934  9414  ltexpri  9424  reclem4pr  9431  fzopth  11730  fzosplit  11839  fzouzsplit  11841  ccatrn  12587  phimullem  14290  prmreclem5  14419  structcnvcnv  14624  imasaddfnlem  14906  imasvscafn  14915  mrcuni  14999  mressmrcd  15005  submrc  15006  ssceq  15176  rescabs  15183  setcepi  15393  clatl  15724  ipopos  15768  psdmrn  15815  psssdm2  15823  dirdm  15842  gsumress  15881  gsumvallem2  15981  gsumwspan  15992  cycsubg  16207  conjnmz  16278  pmtrprfv  16456  symggen  16473  odf1o2  16571  gex1  16589  sylow2alem1  16615  sylow3lem3  16627  lsmidm  16660  lsmss1  16662  lsmss2  16664  lsmmod  16671  lsmdisj  16677  lsmdisj2  16678  cntzcmn  16826  prmcyg  16874  dmdprdd  17008  dprdspan  17052  dprdres  17053  dprdz  17055  subgdmdprd  17059  subgdprd  17060  dprddisj2  17065  dprddisj2OLD  17066  dprd2dlem1  17068  dprd2da  17069  dmdprdsplit2lem  17072  dprdsplit  17075  ablfacrp  17095  pgpfac1lem3  17106  kerf1hrm  17370  isdrng2  17384  issubdrg  17432  lspun  17611  lspsn  17626  lspsnneg  17630  lsp0  17633  lsslsp  17639  lmhmlsp  17673  lspextmo  17680  lsmsp  17710  lspprabs  17719  lspsnvs  17738  lspdisj  17749  lsmcv  17765  lspsnat  17769  lsppratlem6  17776  lspprat  17777  lbsextlem4  17785  lidl1el  17844  drngnidl  17855  lidldvgen  17881  fidomndrng  17934  mplbas2  18112  mplbas2OLD  18113  cnsubrg  18456  mulgrhm2  18510  mulgrhm2OLD  18513  znrrg  18581  ocvin  18682  ocvlsp  18684  mrccss  18702  pjfo  18723  obs2ss  18737  frlmsslsp  18806  frlmsslspOLD  18807  topsn  19413  eltg4i  19438  unitg  19445  tgtop  19452  tgidm  19459  en2top  19464  basgen  19467  2basgen  19469  fctop  19482  cctop  19484  ppttop  19485  epttop  19487  ntrin  19539  isopn3  19544  opnnei  19598  neiuni  19600  maxlp  19625  clslp  19626  tgrest  19637  resttopon  19639  rest0  19647  restfpw  19657  restcls  19659  restntr  19660  ordtbas2  19669  ordtbas  19670  ordtrest2  19682  cmpcov2  19867  tgcmp  19878  cmpcld  19879  uncmp  19880  cmpfi  19885  bwthOLD  19888  2ndcsep  19937  dis2ndc  19938  restnlly  19960  dislly  19975  comppfsc  20010  kgentopon  20016  kgencmp  20023  kgenidm  20025  iskgen2  20026  kgencn3  20036  ptuni2  20054  ptbasfi  20059  xkouni  20077  txcls  20082  ptclsg  20093  txdis  20110  txindis  20112  txcmplem2  20120  xkopt  20133  txcon  20167  qtopval2  20174  qtopuni  20180  qtoprest  20195  qtopomap  20196  qtopcmap  20197  kqsat  20209  kqcldsat  20211  hmeocls  20246  hmeontr  20247  hmphdis  20274  fgfil  20353  fgabs  20357  trfil1  20364  fgtr  20368  trfg  20369  uzrest  20375  ufilmax  20385  ufileu  20397  filufint  20398  ufildom1  20404  rnelfm  20431  flimfil  20447  uffclsflim  20509  alexsublem  20521  alexsubALTlem3  20526  alexsubALT  20528  ptcmplem2  20530  ptcmplem3  20531  tgpconcompeqg  20587  haustsms2  20612  tgptsmscls  20629  ust0  20699  ustbas2  20705  restutopopn  20718  unirnblps  20899  unirnbl  20900  iccntr  21303  pi1xfrcnv  21534  clsocv  21667  cfilfcls  21690  equivcmet  21731  pjth  21831  hlhil  21835  evthicc2  21849  ovolshft  21899  volsup  21943  dyadmbllem  21985  opnmbllem  21987  mbfconstlem  22013  itg11  22075  limciun  22275  dvidlem  22296  dvnres  22311  cpnord  22315  dvaddf  22322  dvmulf  22323  dvcmulf  22325  dvcof  22328  dvcj  22330  dvrec  22335  dvmptcmul  22344  dvcnv  22355  dvcnvre  22397  ftc1cn  22421  plyco0  22566  taylthlem1  22744  taylthlem2  22745  ulmdvlem3  22773  ulmdv  22774  pserdv  22800  wilthlem2  23319  ppisval  23353  ppisval2  23354  ppinprm  23402  chtnprm  23404  umgraex  24299  ubthlem1  25762  pjhth  26287  ococin  26302  chsupsn  26307  ssjo  26341  chabs1  26410  spansncvi  26546  mdslj1i  27214  mdslj2i  27215  atomli  27277  atcvatlem  27280  atcvat3i  27291  sumdmdlem  27313  reff  27819  cmpcref  27830  xpinpreima2  27866  ordtrest2NEW  27882  sigagenid  28128  imambfm  28210  dya2iocuni  28231  sconpi1  28661  cvmsss2  28696  cvmliftlem15  28720  dfrtrcl2  29048  preddowncl  29251  wfi  29262  dftrpred3g  29291  trpredpo  29293  frind  29298  wfrlem10  29327  sltval2  29391  nofulllem5  29441  altopthsn  29586  opnmbllem0  30025  ftc1cnnc  30064  opnbnd  30118  opnregcld  30123  cldregopn  30124  fnessref  30150  neibastop1  30152  topmeet  30157  topjoin  30158  fnemeet1  30159  fnejoin1  30161  fdc  30213  sstotbnd2  30245  isbnd2  30254  totbndbnd  30260  prdstotbnd  30265  heibor1  30281  1idl  30398  igenval2  30438  ismrcd1  30605  ismrcd2  30606  isnacs3  30617  nacsfix  30619  kercvrlsm  31004  pwssplit4  31010  hbtlem5  31052  rgspnid  31097  iocinico  31155  nzin  31199  icoiccdif  31500  lptioo2  31545  lptioo1  31546  fourierdlem79  31857  fzoopth  32178  lspeqlco  32775  bnj1136  33786  bnj1398  33823  bnj1408  33825  bnj1498  33850  lshpdisj  34452  lssats  34477  lsatcvat3  34517  lkrlsp  34567  lshpset2N  34584  lfl1dim  34586  lfl1dim2N  34587  lkrpssN  34628  paddass  35302  paddidm  35305  pmod1i  35312  pmapjat1  35317  pclbtwnN  35361  pclunN  35362  paddunN  35391  pclfinclN  35414  cdleme50rnlem  36010  dihjust  36684  dihmeetlem1N  36757  dihglblem5apreN  36758  dihmeetlem13N  36786  dochocsp  36846  dochdmj1  36857  dochnoncon  36858  dihjatb  36883  dihjat1lem  36895  lcfl9a  36972  lclkrlem2s  36992  lclkrlem2v  36995  mapdrvallem3  37113  mapdunirnN  37117  mapdin  37129  mapdlsm  37131  baerlem3lem2  37177  baerlem5alem2  37178  baerlem5blem2  37179  hdmaprnN  37334  hgmaprnN  37371  hdmaplkr  37383
  Copyright terms: Public domain W3C validator