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

Theorem eqssd 3458
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 3456 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3sylanbrc 662 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1405    C_ wss 3413
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-clab 2388  df-cleq 2394  df-clel 2397  df-in 3420  df-ss 3427
This theorem is referenced by:  eqrd  3459  uneqdifeq  3859  unissel  4220  intmin  4246  unissint  4251  int0el  4258  dmcosseq  5084  sofld  5271  relfld  5348  preddowncl  5393  wfi  5399  tz7.7  5435  fimacnv  5996  knatar  6235  sorpssuni  6570  sorpssint  6571  onint  6612  fo2ndf  6890  suppimacnv  6912  tposeq  6959  wfrlem10  7029  onfununi  7044  tfrlem15  7094  oaass  7246  odi  7264  omass  7265  oelim2  7280  oeeui  7287  nnawordex  7322  oaabslem  7328  oaabs2  7330  omabslem  7331  omabs  7332  uniinqs  7427  sucdom2  7750  fineqv  7769  dffi2  7916  fiuni  7921  dffi3  7924  ordtypelem9  7984  ordtypelem10  7985  oismo  7998  hartogslem1  8000  ixpiunwdom  8050  cantnfp1lem3  8130  oemapvali  8134  cantnf  8143  cantnfp1lem3OLD  8156  cantnfOLD  8165  r1val1  8235  rankval3b  8275  rankunb  8299  rankuni2b  8302  rankr1id  8311  rankc2  8320  rankxplim  8328  tcrank  8333  carden2b  8379  harval2  8409  en2other2  8418  infpwfien  8474  coflim  8672  cfcof  8685  cfidm  8686  isf32lem2  8765  fin1a2lem11  8821  fin1a2lem13  8823  ttukeylem7  8926  fpwwe2  9050  winafp  9104  wuncidm  9153  wuncval2  9154  tskuni  9190  grur1  9227  distrpr  9435  prlem934  9440  ltexpri  9450  reclem4pr  9457  fzopth  11773  fzosplit  11888  fzouzsplit  11890  ccatrn  12658  cotrtrclfv  12993  dmtrclfv  12999  dfrtrcl2  13042  phimullem  14516  prmreclem5  14645  structcnvcnv  14850  imasaddfnlem  15140  imasvscafn  15149  mrcuni  15233  mressmrcd  15239  submrc  15240  ssceq  15437  rescabs  15444  setcepi  15689  clatl  16068  ipopos  16112  psdmrn  16159  psssdm2  16167  dirdm  16186  gsumress  16225  gsumvallem2  16325  gsumwspan  16336  cycsubg  16551  conjnmz  16622  pmtrprfv  16800  symggen  16817  odf1o2  16915  gex1  16933  sylow2alem1  16959  sylow3lem3  16971  lsmidm  17004  lsmss1  17006  lsmss2  17008  lsmmod  17015  lsmdisj  17021  lsmdisj2  17022  cntzcmn  17170  prmcyg  17218  dmdprdd  17348  dprdspan  17392  dprdres  17393  dprdz  17395  subgdmdprd  17399  subgdprd  17400  dprddisj2  17405  dprddisj2OLD  17406  dprd2dlem1  17408  dprd2da  17409  dmdprdsplit2lem  17412  dprdsplit  17415  ablfacrp  17435  pgpfac1lem3  17446  kerf1hrm  17710  isdrng2  17724  issubdrg  17772  lspun  17951  lspsn  17966  lspsnneg  17970  lsp0  17973  lsslsp  17979  lmhmlsp  18013  lspextmo  18020  lsmsp  18050  lspprabs  18059  lspsnvs  18078  lspdisj  18089  lsmcv  18105  lspsnat  18109  lsppratlem6  18116  lspprat  18117  lbsextlem4  18125  lidl1el  18184  drngnidl  18195  lidldvgen  18221  fidomndrng  18274  mplbas2  18452  mplbas2OLD  18453  cnsubrg  18796  mulgrhm2  18834  znrrg  18900  ocvin  19001  ocvlsp  19003  mrccss  19021  pjfo  19042  obs2ss  19056  frlmsslsp  19121  topsn  19726  eltg4i  19751  unitg  19758  tgtop  19765  tgidm  19772  en2top  19777  basgen  19780  2basgen  19782  fctop  19795  cctop  19797  ppttop  19798  epttop  19800  ntrin  19852  isopn3  19858  opnnei  19912  neiuni  19914  maxlp  19939  clslp  19940  tgrest  19951  resttopon  19953  rest0  19961  restfpw  19971  restcls  19973  restntr  19974  ordtbas2  19983  ordtbas  19984  ordtrest2  19996  cmpcov2  20181  tgcmp  20192  cmpcld  20193  uncmp  20194  cmpfi  20199  2ndcsep  20250  dis2ndc  20251  restnlly  20273  dislly  20288  comppfsc  20323  kgentopon  20329  kgencmp  20336  kgenidm  20338  iskgen2  20339  kgencn3  20349  ptuni2  20367  ptbasfi  20372  xkouni  20390  txcls  20395  ptclsg  20406  txdis  20423  txindis  20425  txcmplem2  20433  xkopt  20446  txcon  20480  qtopval2  20487  qtopuni  20493  qtoprest  20508  qtopomap  20509  qtopcmap  20510  kqsat  20522  kqcldsat  20524  hmeocls  20559  hmeontr  20560  hmphdis  20587  fgfil  20666  fgabs  20670  trfil1  20677  fgtr  20681  trfg  20682  uzrest  20688  ufilmax  20698  ufileu  20710  filufint  20711  ufildom1  20717  rnelfm  20744  flimfil  20760  uffclsflim  20822  alexsublem  20834  alexsubALTlem3  20839  alexsubALT  20841  ptcmplem2  20843  ptcmplem3  20844  tgpconcompeqg  20900  haustsms2  20925  tgptsmscls  20942  ust0  21012  ustbas2  21018  restutopopn  21031  unirnblps  21212  unirnbl  21213  iccntr  21616  pi1xfrcnv  21847  clsocv  21980  cfilfcls  22003  equivcmet  22044  pjth  22144  hlhil  22148  evthicc2  22162  ovolshft  22212  volsup  22256  dyadmbllem  22298  opnmbllem  22300  mbfconstlem  22326  itg11  22388  limciun  22588  dvidlem  22609  dvnres  22624  cpnord  22628  dvaddf  22635  dvmulf  22636  dvcmulf  22638  dvcof  22641  dvcj  22643  dvrec  22648  dvmptcmul  22657  dvcnv  22668  dvcnvre  22710  ftc1cn  22734  plyco0  22879  taylthlem1  23058  taylthlem2  23059  ulmdvlem3  23087  ulmdv  23088  pserdv  23114  wilthlem2  23722  ppisval  23756  ppisval2  23757  ppinprm  23805  chtnprm  23807  umgraex  24727  ubthlem1  26186  pjhth  26711  ococin  26726  chsupsn  26731  ssjo  26765  chabs1  26834  spansncvi  26970  mdslj1i  27637  mdslj2i  27638  atomli  27700  atcvatlem  27703  atcvat3i  27714  sumdmdlem  27736  reff  28281  cmpcref  28292  xpinpreima2  28328  ordtrest2NEW  28344  sigagenid  28585  imambfm  28696  dya2iocuni  28717  bnj1136  29367  bnj1398  29404  bnj1408  29406  bnj1498  29431  sconpi1  29523  cvmsss2  29558  cvmliftlem15  29582  dftrpred3g  30034  trpredpo  30036  frind  30041  sltval2  30103  nofulllem5  30153  altopthsn  30286  opnbnd  30540  opnregcld  30545  cldregopn  30546  fnessref  30572  neibastop1  30574  topmeet  30579  topjoin  30580  fnemeet1  30581  fnejoin1  30583  dissneqlem  31243  opnmbllem0  31402  ftc1cnnc  31442  fdc  31500  sstotbnd2  31532  isbnd2  31541  totbndbnd  31547  prdstotbnd  31552  heibor1  31568  1idl  31685  igenval2  31725  lshpdisj  31985  lssats  32010  lsatcvat3  32050  lkrlsp  32100  lshpset2N  32117  lfl1dim  32119  lfl1dim2N  32120  lkrpssN  32161  paddass  32835  paddidm  32838  pmod1i  32845  pmapjat1  32850  pclbtwnN  32894  pclunN  32895  paddunN  32924  pclfinclN  32947  cdleme50rnlem  33543  dihjust  34217  dihmeetlem1N  34290  dihglblem5apreN  34291  dihmeetlem13N  34319  dochocsp  34379  dochdmj1  34390  dochnoncon  34391  dihjatb  34416  dihjat1lem  34428  lcfl9a  34505  lclkrlem2s  34525  lclkrlem2v  34528  mapdrvallem3  34646  mapdunirnN  34650  mapdin  34662  mapdlsm  34664  baerlem3lem2  34710  baerlem5alem2  34711  baerlem5blem2  34712  hdmaprnN  34867  hgmaprnN  34904  hdmaplkr  34916  rntrclfvOAI  34965  ismrcd1  34972  ismrcd2  34973  isnacs3  34984  nacsfix  34986  kercvrlsm  35371  pwssplit4  35377  hbtlem5  35421  rgspnid  35465  iocinico  35523  cbviuneq12df  35620  dfrcl2  35633  dftrcl3  35679  brtrclfv2  35686  dfrtrcl3  35692  nzin  36051  icoiccdif  36913  lptioo2  36986  lptioo1  36987  fourierdlem79  37317  fzoopth  37952  lspeqlco  38532
  Copyright terms: Public domain W3C validator