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

Theorem eqssd 3351
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 3349 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3sylanbrc 647 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    C_ wss 3306
This theorem is referenced by:  eqrd  3352  uneqdifeq  3740  unissel  4068  intmin  4094  unissint  4098  int0el  4105  tz7.7  4636  reusv6OLD  4763  onint  4804  dmcosseq  5166  sofld  5347  relfld  5424  fimacnv  5891  knatar  6109  fo2ndf  6482  tposeq  6510  sorpssuni  6560  sorpssint  6561  onfununi  6632  tfrlem15  6682  oaass  6833  odi  6851  omass  6852  oelim2  6867  oeeui  6874  nnawordex  6909  oaabslem  6915  oaabs2  6917  omabslem  6918  omabs  6919  uniinqs  7013  sucdom2  7332  fineqv  7353  dffi2  7457  fiuni  7462  dffi3  7465  ordtypelem9  7524  ordtypelem10  7525  oismo  7538  hartogslem1  7540  ixpiunwdom  7588  cantnfp1lem3  7665  oemapvali  7669  cantnf  7678  r1val1  7741  rankval3b  7781  rankunb  7805  rankuni2b  7808  rankr1id  7817  rankc2  7826  rankxplim  7834  tcrank  7839  carden2b  7885  harval2  7915  infpwfien  7974  coflim  8172  cfcof  8185  cfidm  8186  isf32lem2  8265  fin1a2lem11  8321  fin1a2lem13  8323  ttukeylem7  8426  fpwwe2  8549  winafp  8603  wuncidm  8652  wuncval2  8653  tskuni  8689  grur1  8726  distrpr  8936  prlem934  8941  ltexpri  8951  reclem4pr  8958  fzopth  11120  fzosplit  11197  fzouzsplit  11199  phimullem  13199  prmreclem5  13319  structcnvcnv  13511  imasaddfnlem  13784  imasvscafn  13793  mrcuni  13877  mressmrcd  13883  submrc  13884  ssceq  14057  rescabs  14064  setcepi  14274  ipopos  14617  psdmrn  14670  psssdm2  14678  dirdm  14710  gsumvallem2  14803  gsumress  14808  gsumwspan  14822  cycsubg  14999  conjnmz  15070  odf1o2  15238  gex1  15256  sylow2alem1  15282  sylow3lem3  15294  lsmidm  15327  lsmss1  15329  lsmss2  15331  lsmmod  15338  lsmdisj  15344  lsmdisj2  15345  cntzcmn  15490  prmcyg  15534  dmdprdd  15591  dprdspan  15616  dprdres  15617  dprdz  15619  subgdmdprd  15623  subgdprd  15624  dprddisj2  15628  dprd2dlem1  15630  dprd2da  15631  dmdprdsplit2lem  15634  dprdsplit  15637  ablfacrp  15655  pgpfac1lem3  15666  isdrng2  15876  issubdrg  15924  lspun  16094  lspsn  16109  lspsnneg  16113  lsp0  16116  lsslsp  16122  lmhmlsp  16156  lspextmo  16163  lsmsp  16189  lspprabs  16198  lspsnvs  16217  lspdisj  16228  lsmcv  16244  lspsnat  16248  lsppratlem6  16255  lspprat  16256  lbsextlem4  16264  lidl1el  16320  drngnidl  16331  lidldvgen  16357  fidomndrng  16398  mplbas2  16562  cnsubrg  16790  mulgrhm2  16819  znrrg  16877  ocvin  16932  ocvlsp  16934  mrccss  16952  pjfo  16973  obs2ss  16987  topsn  17031  eltg4i  17056  tgtop  17069  tgidm  17076  en2top  17081  basgen  17084  2basgen  17086  fctop  17099  cctop  17101  ppttop  17102  epttop  17104  ntrin  17156  isopn3  17161  opnnei  17215  neiuni  17217  maxlp  17242  clslp  17243  tgrest  17254  resttopon  17256  rest0  17264  restfpw  17274  restcls  17276  restntr  17277  ordtbas2  17286  ordtbas  17287  ordtrest2  17299  cmpcov2  17484  tgcmp  17495  cmpcld  17496  uncmp  17497  cmpfi  17502  bwth  17504  2ndcsep  17553  dis2ndc  17554  restnlly  17576  dislly  17591  kgentopon  17601  kgencmp  17608  kgenidm  17610  iskgen2  17611  kgencn3  17621  ptuni2  17639  ptbasfi  17644  xkouni  17662  txcls  17667  ptclsg  17678  txdis  17695  txindis  17697  txcmplem2  17705  xkopt  17718  txcon  17752  qtopval2  17759  qtopuni  17765  qtoprest  17780  qtopomap  17781  qtopcmap  17782  kqsat  17794  kqcldsat  17796  hmeocls  17831  hmeontr  17832  hmphdis  17859  fgfil  17938  fgabs  17942  trfil1  17949  fgtr  17953  trfg  17954  uzrest  17960  ufilmax  17970  ufileu  17982  filufint  17983  ufildom1  17989  rnelfm  18016  flimfil  18032  uffclsflim  18094  alexsublem  18106  alexsubALTlem3  18111  alexsubALT  18113  ptcmplem2  18115  ptcmplem3  18116  tgpconcompeqg  18172  haustsms2  18197  tgptsmscls  18210  ust0  18280  ustbas2  18286  restutopopn  18299  unirnblps  18480  unirnbl  18481  iccntr  18883  pi1xfrcnv  19113  clsocv  19235  cfilfcls  19258  equivcmet  19299  pjth  19371  hlhil  19375  evthicc2  19388  ovolshft  19438  volsup  19481  dyadmbllem  19522  opnmbllem  19524  mbfconstlem  19550  itg11  19612  limciun  19812  dvidlem  19833  dvnres  19848  cpnord  19852  dvaddf  19859  dvmulf  19860  dvcmulf  19862  dvcof  19865  dvcj  19867  dvrec  19872  dvmptcmul  19881  dvcnv  19892  dvcnvre  19934  ftc1cn  19958  plyco0  20142  taylthlem1  20320  taylthlem2  20321  ulmdvlem3  20349  ulmdv  20350  pserdv  20376  wilthlem2  20883  ppisval  20917  ppisval2  20918  ppinprm  20966  chtnprm  20968  umgraex  21389  ubthlem1  22403  pjhth  22926  ococin  22941  chsupsn  22946  ssjo  22980  chabs1  23049  spansncvi  23185  mdslj1i  23853  mdslj2i  23854  atomli  23916  atcvatlem  23919  atcvat3i  23930  sumdmdlem  23952  kerf1hrm  24293  xpinpreima2  24336  sigagenid  24565  imambfm  24643  dya2iocuni  24664  sconpi1  24957  cvmsss2  24992  cvmliftlem15  25016  dfrtrcl2  25179  preddowncl  25502  wfi  25513  dftrpred3g  25542  trpredpo  25544  frind  25549  wfrlem10  25578  sltval2  25642  nofulllem5  25692  altopthsn  25837  opnmbllem0  26278  ftc1cnnc  26317  opnbnd  26366  opnregcld  26371  cldregopn  26372  fnessref  26411  comppfsc  26425  neibastop1  26426  topmeet  26431  topjoin  26432  fnemeet1  26433  fnejoin1  26435  fdc  26487  sstotbnd2  26521  isbnd2  26530  totbndbnd  26536  prdstotbnd  26541  heibor1  26557  1idl  26674  igenval2  26714  ismrcd1  26790  ismrcd2  26791  isnacs3  26802  nacsfix  26804  kercvrlsm  27196  pwssplit4  27206  frlmsslsp  27263  hbtlem5  27347  rgspnid  27392  en2other2  27397  pmtrprfv  27411  symggen  27426  fzoopth  28186  bnj1136  29464  bnj1398  29501  bnj1408  29503  bnj1498  29528  lshpdisj  29883  lssats  29908  lsatcvat3  29948  lkrlsp  29998  lshpset2N  30015  lfl1dim  30017  lfl1dim2N  30018  lkrpssN  30059  paddass  30733  paddidm  30736  pmod1i  30743  pmapjat1  30748  pclbtwnN  30792  pclunN  30793  paddunN  30822  pclfinclN  30845  cdleme50rnlem  31439  dihjust  32113  dihmeetlem1N  32186  dihglblem5apreN  32187  dihmeetlem13N  32215  dochocsp  32275  dochdmj1  32286  dochnoncon  32287  dihjatb  32312  dihjat1lem  32324  lcfl9a  32401  lclkrlem2s  32421  lclkrlem2v  32424  mapdrvallem3  32542  mapdunirnN  32546  mapdin  32558  mapdlsm  32560  baerlem3lem2  32606  baerlem5alem2  32607  baerlem5blem2  32608  hdmaprnN  32763  hgmaprnN  32800  hdmaplkr  32812
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1668  ax-8 1689  ax-6 1746  ax-7 1751  ax-11 1763  ax-12 1953  ax-ext 2423
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3313  df-ss 3320
  Copyright terms: Public domain W3C validator