Theorem eqssd 3949

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 3947	. 2 ⊢ (𝐴 = 𝐵 ↔ (𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2726  df-ss 3916

This theorem is referenced by:  eqelssd  3953  uneqdifeq  4443  pweq  4566  unieq  4872  unissel  4893  intmin  4921  unissint  4925  int0el  4932  intidg  5403  dmcosseq  5925  dmcosseqOLD  5926  dmcosseqOLDOLD  5927  imadifssran  6107  sofld  6143  relfld  6231  preddowncl  6288  frpoind  6298  tz7.7  6341  f1imadifssran  6576  knatar  7301  sorpssuni  7675  sorpssint  7676  onint  7733  fo2ndf  8061  suppimacnv  8114  tposeq  8168  frrlem14  8239  onfununi  8271  tfrlem15  8321  oaass  8486  odi  8504  omass  8505  oelim2  8521  oeeui  8528  nnawordex  8563  oaabslem  8573  oaabs2  8575  omabslem  8576  omabs  8577  cofon1  8598  uniinqs  8732  sucdom2  9125  onomeneq  9136  fineqv  9165  dffi2  9324  fiuni  9329  dffi3  9332  hartogslem1  9445  ixpiunwdom  9493  cantnfp1lem3  9587  oemapvali  9591  cantnf  9600  dfttrcl2  9631  frind  9660  r1val1  9696  rankval3b  9736  rankunb  9760  rankuni2b  9763  rankr1id  9772  rankc2  9781  rankxplim  9789  tcrank  9794  carden2b  9877  harval2  9907  en2other2  9917  infpwfien  9970  coflim  10169  cfcof  10182  cfidm  10183  isf32lem2  10262  fin1a2lem11  10318  fin1a2lem13  10320  ttukeylem7  10423  fpwwe2  10552  winafp  10606  wuncidm  10655  wuncval2  10656  tskuni  10692  grur1  10729  distrpr  10937  ltexpri  10952  reclem4pr  10959  fzopth  13475  fzosplit  13606  fzouzsplit  13608  fzoopth  13676  ccatrn  14511  cotrtrclfv  14933  dmtrclfv  14939  dfrtrcl2  14983  structcnvcnv  17078  imasaddfnlem  17447  imasvscafn  17456  mrcuni  17542  mressmrcd  17548  submrc  17549  ssceq  17748  rescabs  17755  setcepi  18010  clatl  18429  ipopos  18457  psdmrn  18494  dirdm  18521  gsumress  18605  gsumvallem2  18757  gsumwspan  18769  trivsubgd  19080  trivsubgsnd  19081  trivnsgd  19099  cycsubg  19135  kerf1ghm  19174  conjnmz  19179  pmtrprfv  19380  symggen  19397  odf1o2  19500  gex1  19518  sylow2alem1  19544  smndlsmidm  19583  lsmss1  19592  lsmss2  19594  lsmmod  19602  lsmdisj  19608  lsmdisj2  19609  cntzcmn  19767  prmcyg  19821  dmdprdd  19928  dprdspan  19956  dprdres  19957  dprdz  19959  subgdmdprd  19963  subgdprd  19964  dprddisj2  19968  dprd2dlem1  19970  dprd2da  19971  dmdprdsplit2lem  19974  dprdsplit  19977  ablfacrp  19995  pgpfac1lem3  20006  issubdrg  20711  lspun  20936  lspsn  20951  lspsnneg  20955  lsp0  20958  lsslsp  20964  lsslspOLD  20965  lmhmlsp  20999  lspextmo  21006  lsmsp  21036  lspprabs  21045  lspsnvs  21067  lspdisj  21078  lsmcv  21094  lspsnat  21098  lsppratlem6  21105  lspprat  21106  lbsextlem4  21114  lidl1el  21179  drngnidl  21196  lidldvgen  21287  cnsubrg  21380  mulgrhm2  21431  znrrg  21518  ocvin  21627  ocvlsp  21629  mrccss  21647  topsn  22873  eltg4i  22902  unitg  22909  tgtop  22915  tgidm  22922  en2top  22927  basgen  22930  2basgen  22932  fctop  22946  cctop  22948  ppttop  22949  epttop  22951  ntrin  23003  isopn3  23008  opnnei  23062  neiuni  23064  maxlp  23089  clslp  23090  tgrest  23101  resttopon  23103  rest0  23111  restcls  23123  restntr  23124  ordtbas2  23133  ordtbas  23134  ordtrest2  23146  cmpcov2  23332  tgcmp  23343  cmpcld  23344  uncmp  23345  cmpfi  23350  dis2ndc  23402  restnlly  23424  dislly  23439  comppfsc  23474  kgentopon  23480  kgencmp  23487  kgenidm  23489  iskgen2  23490  kgencn3  23500  ptuni2  23518  ptbasfi  23523  xkouni  23541  txcls  23546  txdis  23574  txindis  23576  txcmplem2  23584  xkopt  23597  txconn  23631  qtopval2  23638  qtopuni  23644  qtoprest  23659  qtopomap  23660  qtopcmap  23661  kqsat  23673  kqcldsat  23675  hmeocls  23710  hmeontr  23711  hmphdis  23738  fgfil  23817  fgabs  23821  trfil1  23828  fgtr  23832  uzrest  23839  ufilmax  23849  ufileu  23861  filufint  23862  ufildom1  23868  rnelfm  23895  flimfil  23911  uffclsflim  23973  alexsublem  23986  alexsubALTlem3  23991  alexsubALT  23993  ptcmplem2  23995  ptcmplem3  23996  tgpconncompeqg  24054  haustsms2  24079  tgptsmscls  24092  ust0  24162  ustbas2  24167  iccntr  24764  pi1xfrcnv  25011  clsocv  25204  cfilfcls  25228  equivcmet  25271  hlhil  25397  evthicc2  25415  ovolshft  25466  volsup  25511  dyadmbllem  25554  mbfconstlem  25582  itg11  25646  limciun  25849  dvnres  25887  cpnord  25891  dvcmulf  25902  dvmptcmul  25922  dvcnvre  25978  plyco0  26151  taylthlem1  26335  taylthlem2  26336  taylthlem2OLD  26337  ulmdvlem3  26365  wilthlem2  27033  ppisval  27068  ppinprm  27116  chtnprm  27118  sltval2  27622  noextenddif  27634  scutun12  27778  madebdaylemlrcut  27871  bdayiun  27887  cofcut1  27891  negsbday  28026  onsiso  28236  bdayon  28240  bdayn0p1  28327  upgrex  29114  uvtxnbgr  29422  cusgredg  29446  ubthlem1  30894  pjhth  31417  ococin  31432  chsupsn  31437  ssjo  31471  chabs1  31540  spansncvi  31676  mdslj1i  32343  mdslj2i  32344  atomli  32406  atcvatlem  32409  atcvat3i  32420  sumdmdlem  32442  difininv  32541  fnpreimac  32698  pmtrcnelor  33122  cycpmrn  33174  elrgspnlem4  33276  isdrng4  33326  fldgenid  33350  1fldgenq  33353  rspidlid  33405  0ringidl  33451  drngmxidl  33507  drngmxidlr  33508  resssra  33692  dimkerim  33733  fldextrspunlem1  33781  fldextrspunlem2  33783  algextdeglem4  33826  cmpcref  33956  zarcls1  33975  zarclssn  33979  zart0  33985  zarcmplem  33987  xpinpreima2  34013  ordtrest2NEW  34029  sigagenid  34257  imambfm  34368  reprinfz1  34728  bnj1136  35102  bnj1398  35139  bnj1408  35141  bnj1498  35166  rankval4b  35205  r1omhfb  35217  fineqvacALT  35222  r1omhfbregs  35242  sconnpi1  35382  cvmliftlem15  35441  altopthsn  36104  opnbnd  36468  opnregcld  36473  cldregopn  36474  fnessref  36500  neibastop1  36502  topmeet  36507  topjoin  36508  fnemeet1  36509  fnejoin1  36511  bj-gabeqd  37081  bj-restpw  37236  bj-restb  37238  bj-restuni2  37242  dissneqlem  37484  pibt2  37561  lindsenlbs  37755  poimirlem13  37773  poimirlem14  37774  poimirlem15  37775  fdc  37885  sstotbnd2  37914  isbnd2  37923  totbndbnd  37929  prdstotbnd  37934  heibor1  37950  1idl  38166  igenval2  38206  idreseqidinxp  38447  disjdmqs  39002  lshpdisj  39186  lssats  39211  lsatcvat3  39251  lshpset2N  39318  lfl1dim  39320  lfl1dim2N  39321  lkrpssN  39362  paddass  40037  paddidm  40040  pmod1i  40047  pmapjat1  40052  pclbtwnN  40096  pclunN  40097  paddunN  40126  pclfinclN  40149  dihjust  41416  dihmeetlem1N  41489  dihglblem5apreN  41490  dihmeetlem13N  41518  dochocsp  41578  dochdmj1  41589  dochnoncon  41590  dihjatb  41615  dihjat1lem  41627  lcfl9a  41704  lclkrlem2s  41724  lclkrlem2v  41727  mapdrvallem3  41845  mapdunirnN  41849  mapdin  41861  mapdlsm  41863  baerlem3lem2  41909  baerlem5alem2  41910  baerlem5blem2  41911  hdmaplkr  42112  primrootsunit1  42290  sticksstones11  42349  aks6d1c6lem5  42370  unitscyglem4  42391  rntrclfvOAI  42875  ismrcd1  42882  ismrcd2  42883  isnacs3  42894  nacsfix  42896  rgspnid  43352  iocinico  43396  onsupmaxb  43423  onsssupeqcond  43464  oacl2g  43514  omabs2  43516  omcl2  43517  ofoaf  43539  onsucunifi  43554  naddwordnexlem4  43585  harval3  43721  mptrcllem  43796  clcnvlem  43806  dmtrcl  43810  rntrcl  43811  cbviuneq12df  43844  dfrcl2  43857  dftrcl3  43903  brtrclfv2  43910  dfrtrcl3  43916  scottrankd  44431  nzin  44501  iunincfi  45280  founiiun  45365  founiiun0  45376  inmap  45395  difmapsn  45398  funimaeq  45432  iuneqfzuz  45522  supminfrnmpt  45631  supminfxr2  45655  supminfxrrnmpt  45657  pimxrneun  45674  iooiinicc  45730  icomnfinre  45740  iooiinioc  45744  limsupresxr  45952  liminfresxr  45953  limsup10exlem  45958  liminfvalxr  45969  fourierdlem79  46371  rrxsnicc  46486  prsal  46504  issalgend  46524  sge0f1o  46568  caragenuni  46697  caragendifcl  46700  opnvonmbllem2  46819  iinhoiicc  46860  pimconstlt1  46888  pimltpnff  46889  pimiooltgt  46896  pimgtmnf2  46900  pimdecfgtioc  46901  pimincfltioc  46902  pimdecfgtioo  46903  pimincfltioo  46904  preimageiingt  46906  preimaleiinlt  46907  pimgtmnff  46908  sssmf  46924  smflimlem5  46961  smfmullem4  46980  smfpimbor1lem2  46985  smfsuplem1  46997  smfpimne2  47026  fsupdm  47028  finfdm  47032  sprsymrelf1  47684  lspeqlco  48627  iunlub  49008  iinglb  49009  iuneqconst2  49010  iineqconst2  49011  isclatd  49170  intubeu  49171  unilbeu  49172  setrecsres  49889