Theorem eqssd 3951

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

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

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 2708

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

This theorem is referenced by:  eqelssd  3955  uneqdifeq  4445  pweq  4568  unieq  4874  unissel  4895  intmin  4923  unissint  4927  int0el  4934  intidg  5405  dmcosseq  5927  dmcosseqOLD  5928  dmcosseqOLDOLD  5929  imadifssran  6109  sofld  6145  relfld  6233  preddowncl  6290  frpoind  6300  tz7.7  6343  f1imadifssran  6578  knatar  7303  sorpssuni  7677  sorpssint  7678  onint  7735  fo2ndf  8063  suppimacnv  8116  tposeq  8170  frrlem14  8241  onfununi  8273  tfrlem15  8323  oaass  8488  odi  8506  omass  8507  oelim2  8523  oeeui  8530  nnawordex  8565  oaabslem  8575  oaabs2  8577  omabslem  8578  omabs  8579  cofon1  8600  uniinqs  8734  sucdom2  9127  onomeneq  9138  fineqv  9167  dffi2  9326  fiuni  9331  dffi3  9334  hartogslem1  9447  ixpiunwdom  9495  cantnfp1lem3  9589  oemapvali  9593  cantnf  9602  dfttrcl2  9633  frind  9662  r1val1  9698  rankval3b  9738  rankunb  9762  rankuni2b  9765  rankr1id  9774  rankc2  9783  rankxplim  9791  tcrank  9796  carden2b  9879  harval2  9909  en2other2  9919  infpwfien  9972  coflim  10171  cfcof  10184  cfidm  10185  isf32lem2  10264  fin1a2lem11  10320  fin1a2lem13  10322  ttukeylem7  10425  fpwwe2  10554  winafp  10608  wuncidm  10657  wuncval2  10658  tskuni  10694  grur1  10731  distrpr  10939  ltexpri  10954  reclem4pr  10961  fzopth  13477  fzosplit  13608  fzouzsplit  13610  fzoopth  13678  ccatrn  14513  cotrtrclfv  14935  dmtrclfv  14941  dfrtrcl2  14985  structcnvcnv  17080  imasaddfnlem  17449  imasvscafn  17458  mrcuni  17544  mressmrcd  17550  submrc  17551  ssceq  17750  rescabs  17757  setcepi  18012  clatl  18431  ipopos  18459  psdmrn  18496  dirdm  18523  gsumress  18607  gsumvallem2  18759  gsumwspan  18771  trivsubgd  19082  trivsubgsnd  19083  trivnsgd  19101  cycsubg  19137  kerf1ghm  19176  conjnmz  19181  pmtrprfv  19382  symggen  19399  odf1o2  19502  gex1  19520  sylow2alem1  19546  smndlsmidm  19585  lsmss1  19594  lsmss2  19596  lsmmod  19604  lsmdisj  19610  lsmdisj2  19611  cntzcmn  19769  prmcyg  19823  dmdprdd  19930  dprdspan  19958  dprdres  19959  dprdz  19961  subgdmdprd  19965  subgdprd  19966  dprddisj2  19970  dprd2dlem1  19972  dprd2da  19973  dmdprdsplit2lem  19976  dprdsplit  19979  ablfacrp  19997  pgpfac1lem3  20008  issubdrg  20713  lspun  20938  lspsn  20953  lspsnneg  20957  lsp0  20960  lsslsp  20966  lsslspOLD  20967  lmhmlsp  21001  lspextmo  21008  lsmsp  21038  lspprabs  21047  lspsnvs  21069  lspdisj  21080  lsmcv  21096  lspsnat  21100  lsppratlem6  21107  lspprat  21108  lbsextlem4  21116  lidl1el  21181  drngnidl  21198  lidldvgen  21289  cnsubrg  21382  mulgrhm2  21433  znrrg  21520  ocvin  21629  ocvlsp  21631  mrccss  21649  topsn  22875  eltg4i  22904  unitg  22911  tgtop  22917  tgidm  22924  en2top  22929  basgen  22932  2basgen  22934  fctop  22948  cctop  22950  ppttop  22951  epttop  22953  ntrin  23005  isopn3  23010  opnnei  23064  neiuni  23066  maxlp  23091  clslp  23092  tgrest  23103  resttopon  23105  rest0  23113  restcls  23125  restntr  23126  ordtbas2  23135  ordtbas  23136  ordtrest2  23148  cmpcov2  23334  tgcmp  23345  cmpcld  23346  uncmp  23347  cmpfi  23352  dis2ndc  23404  restnlly  23426  dislly  23441  comppfsc  23476  kgentopon  23482  kgencmp  23489  kgenidm  23491  iskgen2  23492  kgencn3  23502  ptuni2  23520  ptbasfi  23525  xkouni  23543  txcls  23548  txdis  23576  txindis  23578  txcmplem2  23586  xkopt  23599  txconn  23633  qtopval2  23640  qtopuni  23646  qtoprest  23661  qtopomap  23662  qtopcmap  23663  kqsat  23675  kqcldsat  23677  hmeocls  23712  hmeontr  23713  hmphdis  23740  fgfil  23819  fgabs  23823  trfil1  23830  fgtr  23834  uzrest  23841  ufilmax  23851  ufileu  23863  filufint  23864  ufildom1  23870  rnelfm  23897  flimfil  23913  uffclsflim  23975  alexsublem  23988  alexsubALTlem3  23993  alexsubALT  23995  ptcmplem2  23997  ptcmplem3  23998  tgpconncompeqg  24056  haustsms2  24081  tgptsmscls  24094  ust0  24164  ustbas2  24169  iccntr  24766  pi1xfrcnv  25013  clsocv  25206  cfilfcls  25230  equivcmet  25273  hlhil  25399  evthicc2  25417  ovolshft  25468  volsup  25513  dyadmbllem  25556  mbfconstlem  25584  itg11  25648  limciun  25851  dvnres  25889  cpnord  25893  dvcmulf  25904  dvmptcmul  25924  dvcnvre  25980  plyco0  26153  taylthlem1  26337  taylthlem2  26338  taylthlem2OLD  26339  ulmdvlem3  26367  wilthlem2  27035  ppisval  27070  ppinprm  27118  chtnprm  27120  ltsval2  27624  noextenddif  27636  cutsun12  27786  madebdaylemlrcut  27895  bdayiun  27911  cofcut1  27916  negbday  28053  oniso  28267  bdayons  28272  addonbday  28275  bdayn0p1  28365  upgrex  29165  uvtxnbgr  29473  cusgredg  29497  ubthlem1  30945  pjhth  31468  ococin  31483  chsupsn  31488  ssjo  31522  chabs1  31591  spansncvi  31727  mdslj1i  32394  mdslj2i  32395  atomli  32457  atcvatlem  32460  atcvat3i  32471  sumdmdlem  32493  difininv  32592  fnpreimac  32749  pmtrcnelor  33173  cycpmrn  33225  elrgspnlem4  33327  isdrng4  33377  fldgenid  33401  1fldgenq  33404  rspidlid  33456  0ringidl  33502  drngmxidl  33558  drngmxidlr  33559  resssra  33743  dimkerim  33784  fldextrspunlem1  33832  fldextrspunlem2  33834  algextdeglem4  33877  cmpcref  34007  zarcls1  34026  zarclssn  34030  zart0  34036  zarcmplem  34038  xpinpreima2  34064  ordtrest2NEW  34080  sigagenid  34308  imambfm  34419  reprinfz1  34779  bnj1136  35153  bnj1398  35190  bnj1408  35192  bnj1498  35217  rankval4b  35256  r1omhfb  35268  fineqvacALT  35273  r1omhfbregs  35293  sconnpi1  35433  cvmliftlem15  35492  altopthsn  36155  opnbnd  36519  opnregcld  36524  cldregopn  36525  fnessref  36551  neibastop1  36553  topmeet  36558  topjoin  36559  fnemeet1  36560  fnejoin1  36562  bj-gabeqd  37138  bj-restpw  37297  bj-restb  37299  bj-restuni2  37303  dissneqlem  37545  pibt2  37622  lindsenlbs  37816  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  fdc  37946  sstotbnd2  37975  isbnd2  37984  totbndbnd  37990  prdstotbnd  37995  heibor1  38011  1idl  38227  igenval2  38267  idreseqidinxp  38510  disjdmqs  39073  lshpdisj  39257  lssats  39282  lsatcvat3  39322  lshpset2N  39389  lfl1dim  39391  lfl1dim2N  39392  lkrpssN  39433  paddass  40108  paddidm  40111  pmod1i  40118  pmapjat1  40123  pclbtwnN  40167  pclunN  40168  paddunN  40197  pclfinclN  40220  dihjust  41487  dihmeetlem1N  41560  dihglblem5apreN  41561  dihmeetlem13N  41589  dochocsp  41649  dochdmj1  41660  dochnoncon  41661  dihjatb  41686  dihjat1lem  41698  lcfl9a  41775  lclkrlem2s  41795  lclkrlem2v  41798  mapdrvallem3  41916  mapdunirnN  41920  mapdin  41932  mapdlsm  41934  baerlem3lem2  41980  baerlem5alem2  41981  baerlem5blem2  41982  hdmaplkr  42183  primrootsunit1  42361  sticksstones11  42420  aks6d1c6lem5  42441  unitscyglem4  42462  rntrclfvOAI  42943  ismrcd1  42950  ismrcd2  42951  isnacs3  42962  nacsfix  42964  rgspnid  43420  iocinico  43464  onsupmaxb  43491  onsssupeqcond  43532  oacl2g  43582  omabs2  43584  omcl2  43585  ofoaf  43607  onsucunifi  43622  naddwordnexlem4  43653  harval3  43789  mptrcllem  43864  clcnvlem  43874  dmtrcl  43878  rntrcl  43879  cbviuneq12df  43912  dfrcl2  43925  dftrcl3  43971  brtrclfv2  43978  dfrtrcl3  43984  scottrankd  44499  nzin  44569  iunincfi  45348  founiiun  45433  founiiun0  45444  inmap  45463  difmapsn  45466  funimaeq  45500  iuneqfzuz  45590  supminfrnmpt  45699  supminfxr2  45723  supminfxrrnmpt  45725  pimxrneun  45742  iooiinicc  45798  icomnfinre  45808  iooiinioc  45812  limsupresxr  46020  liminfresxr  46021  limsup10exlem  46026  liminfvalxr  46037  fourierdlem79  46439  rrxsnicc  46554  prsal  46572  issalgend  46592  sge0f1o  46636  caragenuni  46765  caragendifcl  46768  opnvonmbllem2  46887  iinhoiicc  46928  pimconstlt1  46956  pimltpnff  46957  pimiooltgt  46964  pimgtmnf2  46968  pimdecfgtioc  46969  pimincfltioc  46970  pimdecfgtioo  46971  pimincfltioo  46972  preimageiingt  46974  preimaleiinlt  46975  pimgtmnff  46976  sssmf  46992  smflimlem5  47029  smfmullem4  47048  smfpimbor1lem2  47053  smfsuplem1  47065  smfpimne2  47094  fsupdm  47096  finfdm  47100  sprsymrelf1  47752  lspeqlco  48695  iunlub  49076  iinglb  49077  iuneqconst2  49078  iineqconst2  49079  isclatd  49238  intubeu  49239  unilbeu  49240  setrecsres  49957