Theorem eqssd 3947

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  eqelssd  3951  uneqdifeq  4442  pweq  4563  unieq  4869  unissel  4890  intmin  4918  unissint  4922  int0el  4929  intidg  5400  dmcosseq  5922  dmcosseqOLD  5923  dmcosseqOLDOLD  5924  imadifssran  6104  sofld  6140  relfld  6228  preddowncl  6285  frpoind  6295  tz7.7  6338  f1imadifssran  6573  knatar  7297  sorpssuni  7671  sorpssint  7672  onint  7729  fo2ndf  8057  suppimacnv  8110  tposeq  8164  frrlem14  8235  onfununi  8267  tfrlem15  8317  oaass  8482  odi  8500  omass  8501  oelim2  8516  oeeui  8523  nnawordex  8558  oaabslem  8568  oaabs2  8570  omabslem  8571  omabs  8572  cofon1  8593  uniinqs  8727  sucdom2  9118  onomeneq  9129  fineqv  9157  dffi2  9313  fiuni  9318  dffi3  9321  hartogslem1  9434  ixpiunwdom  9482  cantnfp1lem3  9576  oemapvali  9580  cantnf  9589  dfttrcl2  9620  frind  9649  r1val1  9685  rankval3b  9725  rankunb  9749  rankuni2b  9752  rankr1id  9761  rankc2  9770  rankxplim  9778  tcrank  9783  carden2b  9866  harval2  9896  en2other2  9906  infpwfien  9959  coflim  10158  cfcof  10171  cfidm  10172  isf32lem2  10251  fin1a2lem11  10307  fin1a2lem13  10309  ttukeylem7  10412  fpwwe2  10540  winafp  10594  wuncidm  10643  wuncval2  10644  tskuni  10680  grur1  10717  distrpr  10925  ltexpri  10940  reclem4pr  10947  fzopth  13467  fzosplit  13598  fzouzsplit  13600  fzoopth  13668  ccatrn  14503  cotrtrclfv  14925  dmtrclfv  14931  dfrtrcl2  14975  structcnvcnv  17070  imasaddfnlem  17438  imasvscafn  17447  mrcuni  17533  mressmrcd  17539  submrc  17540  ssceq  17739  rescabs  17746  setcepi  18001  clatl  18420  ipopos  18448  psdmrn  18485  dirdm  18512  gsumress  18596  gsumvallem2  18748  gsumwspan  18760  trivsubgd  19071  trivsubgsnd  19072  trivnsgd  19090  cycsubg  19126  kerf1ghm  19165  conjnmz  19170  pmtrprfv  19371  symggen  19388  odf1o2  19491  gex1  19509  sylow2alem1  19535  smndlsmidm  19574  lsmss1  19583  lsmss2  19585  lsmmod  19593  lsmdisj  19599  lsmdisj2  19600  cntzcmn  19758  prmcyg  19812  dmdprdd  19919  dprdspan  19947  dprdres  19948  dprdz  19950  subgdmdprd  19954  subgdprd  19955  dprddisj2  19959  dprd2dlem1  19961  dprd2da  19962  dmdprdsplit2lem  19965  dprdsplit  19968  ablfacrp  19986  pgpfac1lem3  19997  issubdrg  20701  lspun  20926  lspsn  20941  lspsnneg  20945  lsp0  20948  lsslsp  20954  lsslspOLD  20955  lmhmlsp  20989  lspextmo  20996  lsmsp  21026  lspprabs  21035  lspsnvs  21057  lspdisj  21068  lsmcv  21084  lspsnat  21088  lsppratlem6  21095  lspprat  21096  lbsextlem4  21104  lidl1el  21169  drngnidl  21186  lidldvgen  21277  cnsubrg  21370  mulgrhm2  21421  znrrg  21508  ocvin  21617  ocvlsp  21619  mrccss  21637  topsn  22852  eltg4i  22881  unitg  22888  tgtop  22894  tgidm  22901  en2top  22906  basgen  22909  2basgen  22911  fctop  22925  cctop  22927  ppttop  22928  epttop  22930  ntrin  22982  isopn3  22987  opnnei  23041  neiuni  23043  maxlp  23068  clslp  23069  tgrest  23080  resttopon  23082  rest0  23090  restcls  23102  restntr  23103  ordtbas2  23112  ordtbas  23113  ordtrest2  23125  cmpcov2  23311  tgcmp  23322  cmpcld  23323  uncmp  23324  cmpfi  23329  dis2ndc  23381  restnlly  23403  dislly  23418  comppfsc  23453  kgentopon  23459  kgencmp  23466  kgenidm  23468  iskgen2  23469  kgencn3  23479  ptuni2  23497  ptbasfi  23502  xkouni  23520  txcls  23525  txdis  23553  txindis  23555  txcmplem2  23563  xkopt  23576  txconn  23610  qtopval2  23617  qtopuni  23623  qtoprest  23638  qtopomap  23639  qtopcmap  23640  kqsat  23652  kqcldsat  23654  hmeocls  23689  hmeontr  23690  hmphdis  23717  fgfil  23796  fgabs  23800  trfil1  23807  fgtr  23811  uzrest  23818  ufilmax  23828  ufileu  23840  filufint  23841  ufildom1  23847  rnelfm  23874  flimfil  23890  uffclsflim  23952  alexsublem  23965  alexsubALTlem3  23970  alexsubALT  23972  ptcmplem2  23974  ptcmplem3  23975  tgpconncompeqg  24033  haustsms2  24058  tgptsmscls  24071  ust0  24141  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  27757  madebdaylemlrcut  27850  bdayiun  27866  cofcut1  27870  negsbday  28005  onsiso  28211  bdayon  28215  bdayn0p1  28300  upgrex  29077  uvtxnbgr  29385  cusgredg  29409  ubthlem1  30857  pjhth  31380  ococin  31395  chsupsn  31400  ssjo  31434  chabs1  31503  spansncvi  31639  mdslj1i  32306  mdslj2i  32307  atomli  32369  atcvatlem  32372  atcvat3i  32383  sumdmdlem  32405  difininv  32504  fnpreimac  32660  pmtrcnelor  33067  cycpmrn  33119  elrgspnlem4  33219  isdrng4  33268  fldgenid  33292  1fldgenq  33295  rspidlid  33347  0ringidl  33393  drngmxidl  33449  drngmxidlr  33450  resssra  33606  dimkerim  33647  fldextrspunlem1  33695  fldextrspunlem2  33697  algextdeglem4  33740  cmpcref  33870  zarcls1  33889  zarclssn  33893  zart0  33899  zarcmplem  33901  xpinpreima2  33927  ordtrest2NEW  33943  sigagenid  34171  imambfm  34282  reprinfz1  34642  bnj1136  35016  bnj1398  35053  bnj1408  35055  bnj1498  35080  rankval4b  35118  r1omhfb  35130  r1omhfbregs  35140  fineqvacALT  35147  sconnpi1  35290  cvmliftlem15  35349  altopthsn  36012  opnbnd  36376  opnregcld  36381  cldregopn  36382  fnessref  36408  neibastop1  36410  topmeet  36415  topjoin  36416  fnemeet1  36417  fnejoin1  36419  bj-gabeqd  36988  bj-restpw  37143  bj-restb  37145  bj-restuni2  37149  dissneqlem  37391  pibt2  37468  lindsenlbs  37661  poimirlem13  37679  poimirlem14  37680  poimirlem15  37681  fdc  37791  sstotbnd2  37820  isbnd2  37829  totbndbnd  37835  prdstotbnd  37840  heibor1  37856  1idl  38072  igenval2  38112  idreseqidinxp  38353  disjdmqs  38908  lshpdisj  39092  lssats  39117  lsatcvat3  39157  lshpset2N  39224  lfl1dim  39226  lfl1dim2N  39227  lkrpssN  39268  paddass  39943  paddidm  39946  pmod1i  39953  pmapjat1  39958  pclbtwnN  40002  pclunN  40003  paddunN  40032  pclfinclN  40055  dihjust  41322  dihmeetlem1N  41395  dihglblem5apreN  41396  dihmeetlem13N  41424  dochocsp  41484  dochdmj1  41495  dochnoncon  41496  dihjatb  41521  dihjat1lem  41533  lcfl9a  41610  lclkrlem2s  41630  lclkrlem2v  41633  mapdrvallem3  41751  mapdunirnN  41755  mapdin  41767  mapdlsm  41769  baerlem3lem2  41815  baerlem5alem2  41816  baerlem5blem2  41817  hdmaplkr  42018  primrootsunit1  42196  sticksstones11  42255  aks6d1c6lem5  42276  unitscyglem4  42297  rntrclfvOAI  42789  ismrcd1  42796  ismrcd2  42797  isnacs3  42808  nacsfix  42810  rgspnid  43266  iocinico  43310  onsupmaxb  43337  onsssupeqcond  43378  oacl2g  43428  omabs2  43430  omcl2  43431  ofoaf  43453  onsucunifi  43468  naddwordnexlem4  43499  harval3  43636  mptrcllem  43711  clcnvlem  43721  dmtrcl  43725  rntrcl  43726  cbviuneq12df  43759  dfrcl2  43772  dftrcl3  43818  brtrclfv2  43825  dfrtrcl3  43831  scottrankd  44346  nzin  44416  iunincfi  45196  founiiun  45281  founiiun0  45292  inmap  45311  difmapsn  45314  funimaeq  45348  iuneqfzuz  45439  supminfrnmpt  45548  supminfxr2  45572  supminfxrrnmpt  45574  pimxrneun  45591  iooiinicc  45647  icomnfinre  45657  iooiinioc  45661  limsupresxr  45869  liminfresxr  45870  limsup10exlem  45875  liminfvalxr  45886  fourierdlem79  46288  rrxsnicc  46403  prsal  46421  issalgend  46441  sge0f1o  46485  caragenuni  46614  caragendifcl  46617  opnvonmbllem2  46736  iinhoiicc  46777  pimconstlt1  46805  pimltpnff  46806  pimiooltgt  46813  pimgtmnf2  46817  pimdecfgtioc  46818  pimincfltioc  46819  pimdecfgtioo  46820  pimincfltioo  46821  preimageiingt  46823  preimaleiinlt  46824  pimgtmnff  46825  sssmf  46841  smflimlem5  46878  smfmullem4  46897  smfpimbor1lem2  46902  smfsuplem1  46914  smfpimne2  46943  fsupdm  46945  finfdm  46949  sprsymrelf1  47601  lspeqlco  48545  iunlub  48926  iinglb  48927  iuneqconst2  48928  iineqconst2  48929  isclatd  49088  intubeu  49089  unilbeu  49090  setrecsres  49808