Theorem eqssd 3981

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

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

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 2708

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

This theorem is referenced by:  eqelssd  3985  uneqdifeq  4473  pweq  4594  unieq  4899  unissel  4919  intmin  4949  unissint  4953  int0el  4960  intidg  5437  dmcosseq  5961  dmcosseqOLD  5962  imadifssran  6145  sofld  6181  relfld  6269  preddowncl  6326  frpoind  6336  wfiOLD  6345  tz7.7  6383  f1imadifssran  6627  knatar  7355  sorpssuni  7731  sorpssint  7732  onint  7789  fo2ndf  8125  suppimacnv  8178  tposeq  8232  frrlem14  8303  onfununi  8360  tfrlem15  8411  oaass  8578  odi  8596  omass  8597  oelim2  8612  oeeui  8619  nnawordex  8654  oaabslem  8664  oaabs2  8666  omabslem  8667  omabs  8668  cofon1  8689  uniinqs  8816  sucdom2OLD  9101  sucdom2  9222  onomeneq  9242  fineqv  9276  dffi2  9440  fiuni  9445  dffi3  9448  hartogslem1  9561  ixpiunwdom  9609  cantnfp1lem3  9699  oemapvali  9703  cantnf  9712  dfttrcl2  9743  frind  9769  r1val1  9805  rankval3b  9845  rankunb  9869  rankuni2b  9872  rankr1id  9881  rankc2  9890  rankxplim  9898  tcrank  9903  carden2b  9986  harval2  10016  en2other2  10028  infpwfien  10081  coflim  10280  cfcof  10293  cfidm  10294  isf32lem2  10373  fin1a2lem11  10429  fin1a2lem13  10431  ttukeylem7  10534  fpwwe2  10662  winafp  10716  wuncidm  10765  wuncval2  10766  tskuni  10802  grur1  10839  distrpr  11047  ltexpri  11062  reclem4pr  11069  fzopth  13583  fzosplit  13714  fzouzsplit  13716  fzoopth  13783  ccatrn  14612  cotrtrclfv  15036  dmtrclfv  15042  dfrtrcl2  15086  structcnvcnv  17177  imasaddfnlem  17547  imasvscafn  17556  mrcuni  17638  mressmrcd  17644  submrc  17645  ssceq  17844  rescabs  17851  setcepi  18106  clatl  18523  ipopos  18551  psdmrn  18588  dirdm  18615  gsumress  18665  gsumvallem2  18817  gsumwspan  18829  trivsubgd  19141  trivsubgsnd  19142  trivnsgd  19160  cycsubg  19196  kerf1ghm  19235  conjnmz  19240  pmtrprfv  19439  symggen  19456  odf1o2  19559  gex1  19577  sylow2alem1  19603  smndlsmidm  19642  lsmss1  19651  lsmss2  19653  lsmmod  19661  lsmdisj  19667  lsmdisj2  19668  cntzcmn  19826  prmcyg  19880  dmdprdd  19987  dprdspan  20015  dprdres  20016  dprdz  20018  subgdmdprd  20022  subgdprd  20023  dprddisj2  20027  dprd2dlem1  20029  dprd2da  20030  dmdprdsplit2lem  20033  dprdsplit  20036  ablfacrp  20054  pgpfac1lem3  20065  issubdrg  20745  lspun  20949  lspsn  20964  lspsnneg  20968  lsp0  20971  lsslsp  20977  lsslspOLD  20978  lmhmlsp  21012  lspextmo  21019  lsmsp  21049  lspprabs  21058  lspsnvs  21080  lspdisj  21091  lsmcv  21107  lspsnat  21111  lsppratlem6  21118  lspprat  21119  lbsextlem4  21127  lidl1el  21192  drngnidl  21209  lidldvgen  21300  cnsubrg  21400  mulgrhm2  21444  znrrg  21531  ocvin  21639  ocvlsp  21641  mrccss  21659  topsn  22874  eltg4i  22903  unitg  22910  tgtop  22916  tgidm  22923  en2top  22928  basgen  22931  2basgen  22933  fctop  22947  cctop  22949  ppttop  22950  epttop  22952  ntrin  23004  isopn3  23009  opnnei  23063  neiuni  23065  maxlp  23090  clslp  23091  tgrest  23102  resttopon  23104  rest0  23112  restcls  23124  restntr  23125  ordtbas2  23134  ordtbas  23135  ordtrest2  23147  cmpcov2  23333  tgcmp  23344  cmpcld  23345  uncmp  23346  cmpfi  23351  dis2ndc  23403  restnlly  23425  dislly  23440  comppfsc  23475  kgentopon  23481  kgencmp  23488  kgenidm  23490  iskgen2  23491  kgencn3  23501  ptuni2  23519  ptbasfi  23524  xkouni  23542  txcls  23547  txdis  23575  txindis  23577  txcmplem2  23585  xkopt  23598  txconn  23632  qtopval2  23639  qtopuni  23645  qtoprest  23660  qtopomap  23661  qtopcmap  23662  kqsat  23674  kqcldsat  23676  hmeocls  23711  hmeontr  23712  hmphdis  23739  fgfil  23818  fgabs  23822  trfil1  23829  fgtr  23833  uzrest  23840  ufilmax  23850  ufileu  23862  filufint  23863  ufildom1  23869  rnelfm  23896  flimfil  23912  uffclsflim  23974  alexsublem  23987  alexsubALTlem3  23992  alexsubALT  23994  ptcmplem2  23996  ptcmplem3  23997  tgpconncompeqg  24055  haustsms2  24080  tgptsmscls  24093  ust0  24163  ustbas2  24169  iccntr  24766  pi1xfrcnv  25013  clsocv  25207  cfilfcls  25231  equivcmet  25274  hlhil  25400  evthicc2  25418  ovolshft  25469  volsup  25514  dyadmbllem  25557  mbfconstlem  25585  itg11  25649  limciun  25852  dvnres  25890  cpnord  25894  dvcmulf  25905  dvmptcmul  25925  dvcnvre  25981  plyco0  26154  taylthlem1  26338  taylthlem2  26339  taylthlem2OLD  26340  ulmdvlem3  26368  wilthlem2  27036  ppisval  27071  ppinprm  27119  chtnprm  27121  sltval2  27625  noextenddif  27637  scutun12  27779  madebdaylemlrcut  27867  cofcut1  27885  negsbday  28020  onsiso  28226  bdayon  28230  bdayn0p1  28315  upgrex  29076  uvtxnbgr  29384  cusgredg  29408  ubthlem1  30856  pjhth  31379  ococin  31394  chsupsn  31399  ssjo  31433  chabs1  31502  spansncvi  31638  mdslj1i  32305  mdslj2i  32306  atomli  32368  atcvatlem  32371  atcvat3i  32382  sumdmdlem  32404  difininv  32503  fnpreimac  32654  pmtrcnelor  33107  cycpmrn  33159  elrgspnlem4  33245  isdrng4  33294  fldgenid  33318  1fldgenq  33321  rspidlid  33395  0ringidl  33441  drngmxidl  33497  drngmxidlr  33498  resssra  33632  dimkerim  33672  fldextrspunlem1  33721  fldextrspunlem2  33723  algextdeglem4  33759  cmpcref  33886  zarcls1  33905  zarclssn  33909  zart0  33915  zarcmplem  33917  xpinpreima2  33943  ordtrest2NEW  33959  sigagenid  34187  imambfm  34299  reprinfz1  34659  bnj1136  35033  bnj1398  35070  bnj1408  35072  bnj1498  35097  fineqvacALT  35134  sconnpi1  35266  cvmliftlem15  35325  altopthsn  35984  opnbnd  36348  opnregcld  36353  cldregopn  36354  fnessref  36380  neibastop1  36382  topmeet  36387  topjoin  36388  fnemeet1  36389  fnejoin1  36391  bj-gabeqd  36960  bj-restpw  37115  bj-restb  37117  bj-restuni2  37121  dissneqlem  37363  pibt2  37440  lindsenlbs  37644  poimirlem13  37662  poimirlem14  37663  poimirlem15  37664  fdc  37774  sstotbnd2  37803  isbnd2  37812  totbndbnd  37818  prdstotbnd  37823  heibor1  37839  1idl  38055  igenval2  38095  idreseqidinxp  38332  disjdmqs  38827  lshpdisj  39010  lssats  39035  lsatcvat3  39075  lshpset2N  39142  lfl1dim  39144  lfl1dim2N  39145  lkrpssN  39186  paddass  39862  paddidm  39865  pmod1i  39872  pmapjat1  39877  pclbtwnN  39921  pclunN  39922  paddunN  39951  pclfinclN  39974  dihjust  41241  dihmeetlem1N  41314  dihglblem5apreN  41315  dihmeetlem13N  41343  dochocsp  41403  dochdmj1  41414  dochnoncon  41415  dihjatb  41440  dihjat1lem  41452  lcfl9a  41529  lclkrlem2s  41549  lclkrlem2v  41552  mapdrvallem3  41670  mapdunirnN  41674  mapdin  41686  mapdlsm  41688  baerlem3lem2  41734  baerlem5alem2  41735  baerlem5blem2  41736  hdmaplkr  41937  primrootsunit1  42115  sticksstones11  42174  aks6d1c6lem5  42195  unitscyglem4  42216  rntrclfvOAI  42689  ismrcd1  42696  ismrcd2  42697  isnacs3  42708  nacsfix  42710  rgspnid  43167  iocinico  43211  onsupmaxb  43238  onsssupeqcond  43279  oacl2g  43329  omabs2  43331  omcl2  43332  ofoaf  43354  onsucunifi  43369  naddwordnexlem4  43400  harval3  43537  mptrcllem  43612  clcnvlem  43622  dmtrcl  43626  rntrcl  43627  cbviuneq12df  43660  dfrcl2  43673  dftrcl3  43719  brtrclfv2  43726  dfrtrcl3  43732  scottrankd  44247  nzin  44317  iunincfi  45098  founiiun  45183  founiiun0  45194  inmap  45213  difmapsn  45216  funimaeq  45250  iuneqfzuz  45342  supminfrnmpt  45452  supminfxr2  45476  supminfxrrnmpt  45478  pimxrneun  45495  iooiinicc  45551  icomnfinre  45561  iooiinioc  45565  limsupresxr  45775  liminfresxr  45776  limsup10exlem  45781  liminfvalxr  45792  fourierdlem79  46194  rrxsnicc  46309  prsal  46327  issalgend  46347  sge0f1o  46391  caragenuni  46520  caragendifcl  46523  opnvonmbllem2  46642  iinhoiicc  46683  pimconstlt1  46711  pimltpnff  46712  pimiooltgt  46719  pimgtmnf2  46723  pimdecfgtioc  46724  pimincfltioc  46725  pimdecfgtioo  46726  pimincfltioo  46727  preimageiingt  46729  preimaleiinlt  46730  pimgtmnff  46731  sssmf  46747  smflimlem5  46784  smfmullem4  46803  smfpimbor1lem2  46808  smfsuplem1  46820  smfpimne2  46849  fsupdm  46851  finfdm  46855  sprsymrelf1  47490  lspeqlco  48395  iunlub  48779  iinglb  48780  iuneqconst2  48781  iineqconst2  48782  isclatd  48937  intubeu  48938  unilbeu  48939  setrecsres  49546