Theorem eqssd 3961

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928

This theorem is referenced by:  eqelssd  3965  uneqdifeq  4452  pweq  4573  unieq  4878  unissel  4898  intmin  4928  unissint  4932  int0el  4939  intidg  5412  dmcosseq  5929  dmcosseqOLD  5930  imadifssran  6112  sofld  6148  relfld  6236  preddowncl  6293  frpoind  6303  tz7.7  6346  f1imadifssran  6586  knatar  7314  sorpssuni  7688  sorpssint  7689  onint  7746  fo2ndf  8077  suppimacnv  8130  tposeq  8184  frrlem14  8255  onfununi  8287  tfrlem15  8337  oaass  8502  odi  8520  omass  8521  oelim2  8536  oeeui  8543  nnawordex  8578  oaabslem  8588  oaabs2  8590  omabslem  8591  omabs  8592  cofon1  8613  uniinqs  8747  sucdom2  9144  onomeneq  9155  fineqv  9186  dffi2  9350  fiuni  9355  dffi3  9358  hartogslem1  9471  ixpiunwdom  9519  cantnfp1lem3  9609  oemapvali  9613  cantnf  9622  dfttrcl2  9653  frind  9679  r1val1  9715  rankval3b  9755  rankunb  9779  rankuni2b  9782  rankr1id  9791  rankc2  9800  rankxplim  9808  tcrank  9813  carden2b  9896  harval2  9926  en2other2  9938  infpwfien  9991  coflim  10190  cfcof  10203  cfidm  10204  isf32lem2  10283  fin1a2lem11  10339  fin1a2lem13  10341  ttukeylem7  10444  fpwwe2  10572  winafp  10626  wuncidm  10675  wuncval2  10676  tskuni  10712  grur1  10749  distrpr  10957  ltexpri  10972  reclem4pr  10979  fzopth  13498  fzosplit  13629  fzouzsplit  13631  fzoopth  13699  ccatrn  14530  cotrtrclfv  14954  dmtrclfv  14960  dfrtrcl2  15004  structcnvcnv  17099  imasaddfnlem  17467  imasvscafn  17476  mrcuni  17562  mressmrcd  17568  submrc  17569  ssceq  17768  rescabs  17775  setcepi  18030  clatl  18449  ipopos  18477  psdmrn  18514  dirdm  18541  gsumress  18591  gsumvallem2  18743  gsumwspan  18755  trivsubgd  19067  trivsubgsnd  19068  trivnsgd  19086  cycsubg  19122  kerf1ghm  19161  conjnmz  19166  pmtrprfv  19367  symggen  19384  odf1o2  19487  gex1  19505  sylow2alem1  19531  smndlsmidm  19570  lsmss1  19579  lsmss2  19581  lsmmod  19589  lsmdisj  19595  lsmdisj2  19596  cntzcmn  19754  prmcyg  19808  dmdprdd  19915  dprdspan  19943  dprdres  19944  dprdz  19946  subgdmdprd  19950  subgdprd  19951  dprddisj2  19955  dprd2dlem1  19957  dprd2da  19958  dmdprdsplit2lem  19961  dprdsplit  19964  ablfacrp  19982  pgpfac1lem3  19993  issubdrg  20700  lspun  20925  lspsn  20940  lspsnneg  20944  lsp0  20947  lsslsp  20953  lsslspOLD  20954  lmhmlsp  20988  lspextmo  20995  lsmsp  21025  lspprabs  21034  lspsnvs  21056  lspdisj  21067  lsmcv  21083  lspsnat  21087  lsppratlem6  21094  lspprat  21095  lbsextlem4  21103  lidl1el  21168  drngnidl  21185  lidldvgen  21276  cnsubrg  21369  mulgrhm2  21420  znrrg  21507  ocvin  21616  ocvlsp  21618  mrccss  21636  topsn  22851  eltg4i  22880  unitg  22887  tgtop  22893  tgidm  22900  en2top  22905  basgen  22908  2basgen  22910  fctop  22924  cctop  22926  ppttop  22927  epttop  22929  ntrin  22981  isopn3  22986  opnnei  23040  neiuni  23042  maxlp  23067  clslp  23068  tgrest  23079  resttopon  23081  rest0  23089  restcls  23101  restntr  23102  ordtbas2  23111  ordtbas  23112  ordtrest2  23124  cmpcov2  23310  tgcmp  23321  cmpcld  23322  uncmp  23323  cmpfi  23328  dis2ndc  23380  restnlly  23402  dislly  23417  comppfsc  23452  kgentopon  23458  kgencmp  23465  kgenidm  23467  iskgen2  23468  kgencn3  23478  ptuni2  23496  ptbasfi  23501  xkouni  23519  txcls  23524  txdis  23552  txindis  23554  txcmplem2  23562  xkopt  23575  txconn  23609  qtopval2  23616  qtopuni  23622  qtoprest  23637  qtopomap  23638  qtopcmap  23639  kqsat  23651  kqcldsat  23653  hmeocls  23688  hmeontr  23689  hmphdis  23716  fgfil  23795  fgabs  23799  trfil1  23806  fgtr  23810  uzrest  23817  ufilmax  23827  ufileu  23839  filufint  23840  ufildom1  23846  rnelfm  23873  flimfil  23889  uffclsflim  23951  alexsublem  23964  alexsubALTlem3  23969  alexsubALT  23971  ptcmplem2  23973  ptcmplem3  23974  tgpconncompeqg  24032  haustsms2  24057  tgptsmscls  24070  ust0  24140  ustbas2  24146  iccntr  24743  pi1xfrcnv  24990  clsocv  25183  cfilfcls  25207  equivcmet  25250  hlhil  25376  evthicc2  25394  ovolshft  25445  volsup  25490  dyadmbllem  25533  mbfconstlem  25561  itg11  25625  limciun  25828  dvnres  25866  cpnord  25870  dvcmulf  25881  dvmptcmul  25901  dvcnvre  25957  plyco0  26130  taylthlem1  26314  taylthlem2  26315  taylthlem2OLD  26316  ulmdvlem3  26344  wilthlem2  27012  ppisval  27047  ppinprm  27095  chtnprm  27097  sltval2  27601  noextenddif  27613  scutun12  27756  madebdaylemlrcut  27848  bdayiun  27864  cofcut1  27868  negsbday  28003  onsiso  28209  bdayon  28213  bdayn0p1  28298  upgrex  29072  uvtxnbgr  29380  cusgredg  29404  ubthlem1  30849  pjhth  31372  ococin  31387  chsupsn  31392  ssjo  31426  chabs1  31495  spansncvi  31631  mdslj1i  32298  mdslj2i  32299  atomli  32361  atcvatlem  32364  atcvat3i  32375  sumdmdlem  32397  difininv  32496  fnpreimac  32645  pmtrcnelor  33063  cycpmrn  33115  elrgspnlem4  33212  isdrng4  33261  fldgenid  33285  1fldgenq  33288  rspidlid  33339  0ringidl  33385  drngmxidl  33441  drngmxidlr  33442  resssra  33576  dimkerim  33616  fldextrspunlem1  33663  fldextrspunlem2  33665  algextdeglem4  33703  cmpcref  33833  zarcls1  33852  zarclssn  33856  zart0  33862  zarcmplem  33864  xpinpreima2  33890  ordtrest2NEW  33906  sigagenid  34134  imambfm  34246  reprinfz1  34606  bnj1136  34980  bnj1398  35017  bnj1408  35019  bnj1498  35044  fineqvacALT  35081  sconnpi1  35219  cvmliftlem15  35278  altopthsn  35942  opnbnd  36306  opnregcld  36311  cldregopn  36312  fnessref  36338  neibastop1  36340  topmeet  36345  topjoin  36346  fnemeet1  36347  fnejoin1  36349  bj-gabeqd  36918  bj-restpw  37073  bj-restb  37075  bj-restuni2  37079  dissneqlem  37321  pibt2  37398  lindsenlbs  37602  poimirlem13  37620  poimirlem14  37621  poimirlem15  37622  fdc  37732  sstotbnd2  37761  isbnd2  37770  totbndbnd  37776  prdstotbnd  37781  heibor1  37797  1idl  38013  igenval2  38053  idreseqidinxp  38290  disjdmqs  38789  lshpdisj  38973  lssats  38998  lsatcvat3  39038  lshpset2N  39105  lfl1dim  39107  lfl1dim2N  39108  lkrpssN  39149  paddass  39825  paddidm  39828  pmod1i  39835  pmapjat1  39840  pclbtwnN  39884  pclunN  39885  paddunN  39914  pclfinclN  39937  dihjust  41204  dihmeetlem1N  41277  dihglblem5apreN  41278  dihmeetlem13N  41306  dochocsp  41366  dochdmj1  41377  dochnoncon  41378  dihjatb  41403  dihjat1lem  41415  lcfl9a  41492  lclkrlem2s  41512  lclkrlem2v  41515  mapdrvallem3  41633  mapdunirnN  41637  mapdin  41649  mapdlsm  41651  baerlem3lem2  41697  baerlem5alem2  41698  baerlem5blem2  41699  hdmaplkr  41900  primrootsunit1  42078  sticksstones11  42137  aks6d1c6lem5  42158  unitscyglem4  42179  rntrclfvOAI  42672  ismrcd1  42679  ismrcd2  42680  isnacs3  42691  nacsfix  42693  rgspnid  43150  iocinico  43194  onsupmaxb  43221  onsssupeqcond  43262  oacl2g  43312  omabs2  43314  omcl2  43315  ofoaf  43337  onsucunifi  43352  naddwordnexlem4  43383  harval3  43520  mptrcllem  43595  clcnvlem  43605  dmtrcl  43609  rntrcl  43610  cbviuneq12df  43643  dfrcl2  43656  dftrcl3  43702  brtrclfv2  43709  dfrtrcl3  43715  scottrankd  44230  nzin  44300  iunincfi  45081  founiiun  45166  founiiun0  45177  inmap  45196  difmapsn  45199  funimaeq  45233  iuneqfzuz  45324  supminfrnmpt  45434  supminfxr2  45458  supminfxrrnmpt  45460  pimxrneun  45477  iooiinicc  45533  icomnfinre  45543  iooiinioc  45547  limsupresxr  45757  liminfresxr  45758  limsup10exlem  45763  liminfvalxr  45774  fourierdlem79  46176  rrxsnicc  46291  prsal  46309  issalgend  46329  sge0f1o  46373  caragenuni  46502  caragendifcl  46505  opnvonmbllem2  46624  iinhoiicc  46665  pimconstlt1  46693  pimltpnff  46694  pimiooltgt  46701  pimgtmnf2  46705  pimdecfgtioc  46706  pimincfltioc  46707  pimdecfgtioo  46708  pimincfltioo  46709  preimageiingt  46711  preimaleiinlt  46712  pimgtmnff  46713  sssmf  46729  smflimlem5  46766  smfmullem4  46785  smfpimbor1lem2  46790  smfsuplem1  46802  smfpimne2  46831  fsupdm  46833  finfdm  46837  sprsymrelf1  47490  lspeqlco  48421  iunlub  48802  iinglb  48803  iuneqconst2  48804  iineqconst2  48805  isclatd  48964  intubeu  48965  unilbeu  48966  setrecsres  49684