Theorem eqssd 3953

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	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
eqssd.2	⊢ (𝜑 → 𝐵 ⊆ 𝐴)

Assertion

Ref	Expression
eqssd	⊢ (𝜑 → 𝐴 = 𝐵)

Proof of Theorem eqssd

Step	Hyp	Ref	Expression
1		eqssd.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		eqssd.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		eqss 3951	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	sylanbrc 584	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  eqelssd  3957  uneqdifeq  4447  pweq  4570  unieq  4876  unissel  4897  intmin  4925  unissint  4929  int0el  4936  intidg  5412  dmcosseq  5935  dmcosseqOLD  5936  dmcosseqOLDOLD  5937  imadifssran  6117  sofld  6153  relfld  6241  preddowncl  6298  frpoind  6308  tz7.7  6351  f1imadifssran  6586  knatar  7313  sorpssuni  7687  sorpssint  7688  onint  7745  fo2ndf  8073  suppimacnv  8126  tposeq  8180  frrlem14  8251  onfununi  8283  tfrlem15  8333  oaass  8498  odi  8516  omass  8517  oelim2  8533  oeeui  8540  nnawordex  8575  oaabslem  8585  oaabs2  8587  omabslem  8588  omabs  8589  cofon1  8610  uniinqs  8746  sucdom2  9139  onomeneq  9150  fineqv  9179  dffi2  9338  fiuni  9343  dffi3  9346  hartogslem1  9459  ixpiunwdom  9507  cantnfp1lem3  9601  oemapvali  9605  cantnf  9614  dfttrcl2  9645  frind  9674  r1val1  9710  rankval3b  9750  rankunb  9774  rankuni2b  9777  rankr1id  9786  rankc2  9795  rankxplim  9803  tcrank  9808  carden2b  9891  harval2  9921  en2other2  9931  infpwfien  9984  coflim  10183  cfcof  10196  cfidm  10197  isf32lem2  10276  fin1a2lem11  10332  fin1a2lem13  10334  ttukeylem7  10437  fpwwe2  10566  winafp  10620  wuncidm  10669  wuncval2  10670  tskuni  10706  grur1  10743  distrpr  10951  ltexpri  10966  reclem4pr  10973  fzopth  13489  fzosplit  13620  fzouzsplit  13622  fzoopth  13690  ccatrn  14525  cotrtrclfv  14947  dmtrclfv  14953  dfrtrcl2  14997  structcnvcnv  17092  imasaddfnlem  17461  imasvscafn  17470  mrcuni  17556  mressmrcd  17562  submrc  17563  ssceq  17762  rescabs  17769  setcepi  18024  clatl  18443  ipopos  18471  psdmrn  18508  dirdm  18535  gsumress  18619  gsumvallem2  18771  gsumwspan  18783  trivsubgd  19094  trivsubgsnd  19095  trivnsgd  19113  cycsubg  19149  kerf1ghm  19188  conjnmz  19193  pmtrprfv  19394  symggen  19411  odf1o2  19514  gex1  19532  sylow2alem1  19558  smndlsmidm  19597  lsmss1  19606  lsmss2  19608  lsmmod  19616  lsmdisj  19622  lsmdisj2  19623  cntzcmn  19781  prmcyg  19835  dmdprdd  19942  dprdspan  19970  dprdres  19971  dprdz  19973  subgdmdprd  19977  subgdprd  19978  dprddisj2  19982  dprd2dlem1  19984  dprd2da  19985  dmdprdsplit2lem  19988  dprdsplit  19991  ablfacrp  20009  pgpfac1lem3  20020  issubdrg  20725  lspun  20950  lspsn  20965  lspsnneg  20969  lsp0  20972  lsslsp  20978  lsslspOLD  20979  lmhmlsp  21013  lspextmo  21020  lsmsp  21050  lspprabs  21059  lspsnvs  21081  lspdisj  21092  lsmcv  21108  lspsnat  21112  lsppratlem6  21119  lspprat  21120  lbsextlem4  21128  lidl1el  21193  drngnidl  21210  lidldvgen  21301  cnsubrg  21394  mulgrhm2  21445  znrrg  21532  ocvin  21641  ocvlsp  21643  mrccss  21661  topsn  22887  eltg4i  22916  unitg  22923  tgtop  22929  tgidm  22936  en2top  22941  basgen  22944  2basgen  22946  fctop  22960  cctop  22962  ppttop  22963  epttop  22965  ntrin  23017  isopn3  23022  opnnei  23076  neiuni  23078  maxlp  23103  clslp  23104  tgrest  23115  resttopon  23117  rest0  23125  restcls  23137  restntr  23138  ordtbas2  23147  ordtbas  23148  ordtrest2  23160  cmpcov2  23346  tgcmp  23357  cmpcld  23358  uncmp  23359  cmpfi  23364  dis2ndc  23416  restnlly  23438  dislly  23453  comppfsc  23488  kgentopon  23494  kgencmp  23501  kgenidm  23503  iskgen2  23504  kgencn3  23514  ptuni2  23532  ptbasfi  23537  xkouni  23555  txcls  23560  txdis  23588  txindis  23590  txcmplem2  23598  xkopt  23611  txconn  23645  qtopval2  23652  qtopuni  23658  qtoprest  23673  qtopomap  23674  qtopcmap  23675  kqsat  23687  kqcldsat  23689  hmeocls  23724  hmeontr  23725  hmphdis  23752  fgfil  23831  fgabs  23835  trfil1  23842  fgtr  23846  uzrest  23853  ufilmax  23863  ufileu  23875  filufint  23876  ufildom1  23882  rnelfm  23909  flimfil  23925  uffclsflim  23987  alexsublem  24000  alexsubALTlem3  24005  alexsubALT  24007  ptcmplem2  24009  ptcmplem3  24010  tgpconncompeqg  24068  haustsms2  24093  tgptsmscls  24106  ust0  24176  ustbas2  24181  iccntr  24778  pi1xfrcnv  25025  clsocv  25218  cfilfcls  25242  equivcmet  25285  hlhil  25411  evthicc2  25429  ovolshft  25480  volsup  25525  dyadmbllem  25568  mbfconstlem  25596  itg11  25660  limciun  25863  dvnres  25901  cpnord  25905  dvcmulf  25916  dvmptcmul  25936  dvcnvre  25992  plyco0  26165  taylthlem1  26349  taylthlem2  26350  taylthlem2OLD  26351  ulmdvlem3  26379  wilthlem2  27047  ppisval  27082  ppinprm  27130  chtnprm  27132  ltsval2  27636  noextenddif  27648  cutsun12  27798  madebdaylemlrcut  27907  bdayiun  27923  cofcut1  27928  negbday  28065  oniso  28279  bdayons  28284  addonbday  28287  bdayn0p1  28377  upgrex  29177  uvtxnbgr  29485  cusgredg  29509  ubthlem1  30958  pjhth  31481  ococin  31496  chsupsn  31501  ssjo  31535  chabs1  31604  spansncvi  31740  mdslj1i  32407  mdslj2i  32408  atomli  32470  atcvatlem  32473  atcvat3i  32484  sumdmdlem  32506  difininv  32604  fnpreimac  32760  pmtrcnelor  33185  cycpmrn  33237  elrgspnlem4  33339  isdrng4  33389  fldgenid  33413  1fldgenq  33416  rspidlid  33468  0ringidl  33514  drngmxidl  33570  drngmxidlr  33571  esplyfvaln  33751  resssra  33764  dimkerim  33805  fldextrspunlem1  33853  fldextrspunlem2  33855  algextdeglem4  33898  cmpcref  34028  zarcls1  34047  zarclssn  34051  zart0  34057  zarcmplem  34059  xpinpreima2  34085  ordtrest2NEW  34101  sigagenid  34329  imambfm  34440  reprinfz1  34800  bnj1136  35173  bnj1398  35210  bnj1408  35212  bnj1498  35237  rankval4b  35277  r1omhfb  35290  fineqvacALT  35295  r1omhfbregs  35315  sconnpi1  35455  cvmliftlem15  35514  altopthsn  36177  opnbnd  36541  opnregcld  36546  cldregopn  36547  fnessref  36573  neibastop1  36575  topmeet  36580  topjoin  36581  fnemeet1  36582  fnejoin1  36584  bj-gabeqd  37185  bj-restpw  37345  bj-restb  37347  bj-restuni2  37351  dissneqlem  37595  pibt2  37672  lindsenlbs  37866  poimirlem13  37884  poimirlem14  37885  poimirlem15  37886  fdc  37996  sstotbnd2  38025  isbnd2  38034  totbndbnd  38040  prdstotbnd  38045  heibor1  38061  1idl  38277  igenval2  38317  idreseqidinxp  38566  disjdmqs  39158  lshpdisj  39363  lssats  39388  lsatcvat3  39428  lshpset2N  39495  lfl1dim  39497  lfl1dim2N  39498  lkrpssN  39539  paddass  40214  paddidm  40217  pmod1i  40224  pmapjat1  40229  pclbtwnN  40273  pclunN  40274  paddunN  40303  pclfinclN  40326  dihjust  41593  dihmeetlem1N  41666  dihglblem5apreN  41667  dihmeetlem13N  41695  dochocsp  41755  dochdmj1  41766  dochnoncon  41767  dihjatb  41792  dihjat1lem  41804  lcfl9a  41881  lclkrlem2s  41901  lclkrlem2v  41904  mapdrvallem3  42022  mapdunirnN  42026  mapdin  42038  mapdlsm  42040  baerlem3lem2  42086  baerlem5alem2  42087  baerlem5blem2  42088  hdmaplkr  42289  primrootsunit1  42467  sticksstones11  42526  aks6d1c6lem5  42547  unitscyglem4  42568  rntrclfvOAI  43048  ismrcd1  43055  ismrcd2  43056  isnacs3  43067  nacsfix  43069  rgspnid  43525  iocinico  43569  onsupmaxb  43596  onsssupeqcond  43637  oacl2g  43687  omabs2  43689  omcl2  43690  ofoaf  43712  onsucunifi  43727  naddwordnexlem4  43758  harval3  43894  mptrcllem  43969  clcnvlem  43979  dmtrcl  43983  rntrcl  43984  cbviuneq12df  44017  dfrcl2  44030  dftrcl3  44076  brtrclfv2  44083  dfrtrcl3  44089  scottrankd  44604  nzin  44674  iunincfi  45453  founiiun  45538  founiiun0  45549  inmap  45567  difmapsn  45570  funimaeq  45604  iuneqfzuz  45694  supminfrnmpt  45803  supminfxr2  45827  supminfxrrnmpt  45829  pimxrneun  45846  iooiinicc  45902  icomnfinre  45912  iooiinioc  45916  limsupresxr  46124  liminfresxr  46125  limsup10exlem  46130  liminfvalxr  46141  fourierdlem79  46543  rrxsnicc  46658  prsal  46676  issalgend  46696  sge0f1o  46740  caragenuni  46869  caragendifcl  46872  opnvonmbllem2  46991  iinhoiicc  47032  pimconstlt1  47060  pimltpnff  47061  pimiooltgt  47068  pimgtmnf2  47072  pimdecfgtioc  47073  pimincfltioc  47074  pimdecfgtioo  47075  pimincfltioo  47076  preimageiingt  47078  preimaleiinlt  47079  pimgtmnff  47080  sssmf  47096  smflimlem5  47133  smfmullem4  47152  smfpimbor1lem2  47157  smfsuplem1  47169  smfpimne2  47198  fsupdm  47200  finfdm  47204  sprsymrelf1  47856  lspeqlco  48799  iunlub  49180  iinglb  49181  iuneqconst2  49182  iineqconst2  49183  isclatd  49342  intubeu  49343  unilbeu  49344  setrecsres  50061