Theorem eqssd 3940

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  eqelssd  3944  uneqdifeq  4433  pweq  4556  unieq  4862  unissel  4883  intmin  4911  unissint  4915  int0el  4922  intidg  5405  dmcosseq  5928  dmcosseqOLD  5929  dmcosseqOLDOLD  5930  imadifssran  6110  sofld  6146  relfld  6234  preddowncl  6291  frpoind  6301  tz7.7  6344  f1imadifssran  6579  knatar  7306  sorpssuni  7680  sorpssint  7681  onint  7738  fo2ndf  8065  suppimacnv  8118  tposeq  8172  frrlem14  8243  onfununi  8275  tfrlem15  8325  oaass  8490  odi  8508  omass  8509  oelim2  8525  oeeui  8532  nnawordex  8567  oaabslem  8577  oaabs2  8579  omabslem  8580  omabs  8581  cofon1  8602  uniinqs  8738  sucdom2  9131  onomeneq  9142  fineqv  9171  dffi2  9330  fiuni  9335  dffi3  9338  hartogslem1  9451  ixpiunwdom  9499  cantnfp1lem3  9595  oemapvali  9599  cantnf  9608  dfttrcl2  9639  frind  9668  r1val1  9704  rankval3b  9744  rankunb  9768  rankuni2b  9771  rankr1id  9780  rankc2  9789  rankxplim  9797  tcrank  9802  carden2b  9885  harval2  9915  en2other2  9925  infpwfien  9978  coflim  10177  cfcof  10190  cfidm  10191  isf32lem2  10270  fin1a2lem11  10326  fin1a2lem13  10328  ttukeylem7  10431  fpwwe2  10560  winafp  10614  wuncidm  10663  wuncval2  10664  tskuni  10700  grur1  10737  distrpr  10945  ltexpri  10960  reclem4pr  10967  fzopth  13509  fzosplit  13641  fzouzsplit  13643  fzoopth  13711  ccatrn  14546  cotrtrclfv  14968  dmtrclfv  14974  dfrtrcl2  15018  structcnvcnv  17117  imasaddfnlem  17486  imasvscafn  17495  mrcuni  17581  mressmrcd  17587  submrc  17588  ssceq  17787  rescabs  17794  setcepi  18049  clatl  18468  ipopos  18496  psdmrn  18533  dirdm  18560  gsumress  18644  gsumvallem2  18796  gsumwspan  18808  trivsubgd  19122  trivsubgsnd  19123  trivnsgd  19141  cycsubg  19177  kerf1ghm  19216  conjnmz  19221  pmtrprfv  19422  symggen  19439  odf1o2  19542  gex1  19560  sylow2alem1  19586  smndlsmidm  19625  lsmss1  19634  lsmss2  19636  lsmmod  19644  lsmdisj  19650  lsmdisj2  19651  cntzcmn  19809  prmcyg  19863  dmdprdd  19970  dprdspan  19998  dprdres  19999  dprdz  20001  subgdmdprd  20005  subgdprd  20006  dprddisj2  20010  dprd2dlem1  20012  dprd2da  20013  dmdprdsplit2lem  20016  dprdsplit  20019  ablfacrp  20037  pgpfac1lem3  20048  issubdrg  20751  lspun  20976  lspsn  20991  lspsnneg  20995  lsp0  20998  lsslsp  21004  lsslspOLD  21005  lmhmlsp  21039  lspextmo  21046  lsmsp  21076  lspprabs  21085  lspsnvs  21107  lspdisj  21118  lsmcv  21134  lspsnat  21138  lsppratlem6  21145  lspprat  21146  lbsextlem4  21154  lidl1el  21219  drngnidl  21236  lidldvgen  21327  cnsubrg  21420  mulgrhm2  21471  znrrg  21558  ocvin  21667  ocvlsp  21669  mrccss  21687  topsn  22909  eltg4i  22938  unitg  22945  tgtop  22951  tgidm  22958  en2top  22963  basgen  22966  2basgen  22968  fctop  22982  cctop  22984  ppttop  22985  epttop  22987  ntrin  23039  isopn3  23044  opnnei  23098  neiuni  23100  maxlp  23125  clslp  23126  tgrest  23137  resttopon  23139  rest0  23147  restcls  23159  restntr  23160  ordtbas2  23169  ordtbas  23170  ordtrest2  23182  cmpcov2  23368  tgcmp  23379  cmpcld  23380  uncmp  23381  cmpfi  23386  dis2ndc  23438  restnlly  23460  dislly  23475  comppfsc  23510  kgentopon  23516  kgencmp  23523  kgenidm  23525  iskgen2  23526  kgencn3  23536  ptuni2  23554  ptbasfi  23559  xkouni  23577  txcls  23582  txdis  23610  txindis  23612  txcmplem2  23620  xkopt  23633  txconn  23667  qtopval2  23674  qtopuni  23680  qtoprest  23695  qtopomap  23696  qtopcmap  23697  kqsat  23709  kqcldsat  23711  hmeocls  23746  hmeontr  23747  hmphdis  23774  fgfil  23853  fgabs  23857  trfil1  23864  fgtr  23868  uzrest  23875  ufilmax  23885  ufileu  23897  filufint  23898  ufildom1  23904  rnelfm  23931  flimfil  23947  uffclsflim  24009  alexsublem  24022  alexsubALTlem3  24027  alexsubALT  24029  ptcmplem2  24031  ptcmplem3  24032  tgpconncompeqg  24090  haustsms2  24115  tgptsmscls  24128  ust0  24198  ustbas2  24203  iccntr  24800  pi1xfrcnv  25037  clsocv  25230  cfilfcls  25254  equivcmet  25297  hlhil  25423  evthicc2  25440  ovolshft  25491  volsup  25536  dyadmbllem  25579  mbfconstlem  25607  itg11  25671  limciun  25874  dvnres  25911  cpnord  25915  dvcmulf  25925  dvmptcmul  25944  dvcnvre  25999  plyco0  26170  taylthlem1  26353  taylthlem2  26354  taylthlem2OLD  26355  ulmdvlem3  26383  wilthlem2  27049  ppisval  27084  ppinprm  27132  chtnprm  27134  ltsval2  27637  noextenddif  27649  cutsun12  27799  madebdaylemlrcut  27908  bdayiun  27924  cofcut1  27929  negbday  28066  oniso  28280  bdayons  28285  addonbday  28288  bdayn0p1  28378  upgrex  29178  uvtxnbgr  29486  cusgredg  29510  ubthlem1  30959  pjhth  31482  ococin  31497  chsupsn  31502  ssjo  31536  chabs1  31605  spansncvi  31741  mdslj1i  32408  mdslj2i  32409  atomli  32471  atcvatlem  32474  atcvat3i  32485  sumdmdlem  32507  difininv  32605  fnpreimac  32761  pmtrcnelor  33170  cycpmrn  33222  elrgspnlem4  33324  isdrng4  33374  fldgenid  33398  1fldgenq  33401  rspidlid  33453  0ringidl  33499  drngmxidl  33555  drngmxidlr  33556  esplyfvaln  33736  resssra  33749  dimkerim  33790  fldextrspunlem1  33838  fldextrspunlem2  33840  algextdeglem4  33883  cmpcref  34013  zarcls1  34032  zarclssn  34036  zart0  34042  zarcmplem  34044  xpinpreima2  34070  ordtrest2NEW  34086  sigagenid  34314  imambfm  34425  reprinfz1  34785  bnj1136  35158  bnj1398  35195  bnj1408  35197  bnj1498  35222  rankval4b  35262  r1omhfb  35275  fineqvacALT  35280  r1omhfbregs  35300  sconnpi1  35440  cvmliftlem15  35499  altopthsn  36162  opnbnd  36526  opnregcld  36531  cldregopn  36532  fnessref  36558  neibastop1  36560  topmeet  36565  topjoin  36566  fnemeet1  36567  fnejoin1  36569  ttctrid  36703  dfttc2g  36707  dfttc3gw  36724  bj-gabeqd  37263  bj-restpw  37423  bj-restb  37425  bj-restuni2  37429  dissneqlem  37673  pibt2  37750  lindsenlbs  37953  poimirlem13  37971  poimirlem14  37972  poimirlem15  37973  fdc  38083  sstotbnd2  38112  isbnd2  38121  totbndbnd  38127  prdstotbnd  38132  heibor1  38148  1idl  38364  igenval2  38404  idreseqidinxp  38653  disjdmqs  39245  lshpdisj  39450  lssats  39475  lsatcvat3  39515  lshpset2N  39582  lfl1dim  39584  lfl1dim2N  39585  lkrpssN  39626  paddass  40301  paddidm  40304  pmod1i  40311  pmapjat1  40316  pclbtwnN  40360  pclunN  40361  paddunN  40390  pclfinclN  40413  dihjust  41680  dihmeetlem1N  41753  dihglblem5apreN  41754  dihmeetlem13N  41782  dochocsp  41842  dochdmj1  41853  dochnoncon  41854  dihjatb  41879  dihjat1lem  41891  lcfl9a  41968  lclkrlem2s  41988  lclkrlem2v  41991  mapdrvallem3  42109  mapdunirnN  42113  mapdin  42125  mapdlsm  42127  baerlem3lem2  42173  baerlem5alem2  42174  baerlem5blem2  42175  hdmaplkr  42376  primrootsunit1  42553  sticksstones11  42612  aks6d1c6lem5  42633  unitscyglem4  42654  rntrclfvOAI  43140  ismrcd1  43147  ismrcd2  43148  isnacs3  43159  nacsfix  43161  rgspnid  43617  iocinico  43661  onsupmaxb  43688  onsssupeqcond  43729  oacl2g  43779  omabs2  43781  omcl2  43782  ofoaf  43804  onsucunifi  43819  naddwordnexlem4  43850  harval3  43986  mptrcllem  44061  clcnvlem  44071  dmtrcl  44075  rntrcl  44076  cbviuneq12df  44109  dfrcl2  44122  dftrcl3  44168  brtrclfv2  44175  dfrtrcl3  44181  scottrankd  44696  nzin  44766  iunincfi  45545  founiiun  45630  founiiun0  45641  inmap  45659  difmapsn  45662  funimaeq  45696  iuneqfzuz  45786  supminfrnmpt  45894  supminfxr2  45918  supminfxrrnmpt  45920  pimxrneun  45937  iooiinicc  45993  icomnfinre  46003  iooiinioc  46007  limsupresxr  46215  liminfresxr  46216  limsup10exlem  46221  liminfvalxr  46232  fourierdlem79  46634  rrxsnicc  46749  prsal  46767  issalgend  46787  sge0f1o  46831  caragenuni  46960  caragendifcl  46963  opnvonmbllem2  47082  iinhoiicc  47123  pimconstlt1  47151  pimltpnff  47152  pimiooltgt  47159  pimgtmnf2  47163  pimdecfgtioc  47164  pimincfltioc  47165  pimdecfgtioo  47166  pimincfltioo  47167  preimageiingt  47169  preimaleiinlt  47170  pimgtmnff  47171  sssmf  47187  smflimlem5  47224  smfmullem4  47243  smfpimbor1lem2  47248  smfsuplem1  47260  smfpimne2  47289  fsupdm  47291  finfdm  47295  sprsymrelf1  47971  lspeqlco  48930  iunlub  49311  iinglb  49312  iuneqconst2  49313  iineqconst2  49314  isclatd  49473  intubeu  49474  unilbeu  49475  setrecsres  50192