Theorem eqssd 3948

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  eqelssd  3952  uneqdifeq  4448  pweq  4571  unieq  4878  unissel  4900  intmin  4928  unissint  4932  int0el  4939  intidg  5425  dmcosseq  5960  dmcosseqOLD  5961  sofld  6179  imadifssranOLD  6202  imadifssranOLDOLD  6203  relfld  6277  preddowncl  6335  frpoind  6345  tz7.7  6388  knatar  7367  sorpssuni  7748  sorpssint  7749  onint  7804  fo2ndf  8132  suppimacnv  8191  tposeq  8245  frrlem14  8317  onfununi  8349  tfrlem15  8400  oaass  8569  odi  8587  omass  8588  oelim2  8604  oeeui  8611  nnawordex  8646  oaabslem  8656  oaabs2  8658  omabslem  8659  omabs  8660  cofon1  8681  uniinqs  8818  sucdom2  9218  onomeneq  9229  fineqv  9258  dffi2  9415  fiuni  9420  dffi3  9423  hartogslem1  9536  ixpiunwdom  9584  cantnfp1lem3  9681  oemapvali  9685  cantnf  9694  dfttrcl2  9725  frind  9754  r1val1  9793  rankval3b  9836  rankunb  9864  rankuni2b  9867  rankr1id  9878  rankval4b  9880  rankc2  9888  rankxplim  9896  tcrank  9901  scottrankd  9949  carden2b  10048  harval2  10078  en2other2  10088  infpwfien  10141  coflim  10339  cfcof  10352  cfidm  10353  isf32lem2  10432  fin1a2lem11  10488  fin1a2lem13  10490  ttukeylem7  10593  fpwwe2  10728  winafp  10782  wuncidm  10831  wuncval2  10832  tskuni  10868  grur1  10905  distrpr  11113  ltexpri  11128  reclem4pr  11135  fzopth  13695  fzosplit  13827  fzouzsplit  13829  fzoopth  13897  ccatrn  14735  cotrtrclfv  15165  dmtrclfv  15171  dfrtrcl2  15215  structcnvcnv  17331  imasaddfnlem  17700  imasvscafn  17709  mrcuni  17795  mressmrcd  17801  submrc  17802  ssceq  18001  rescabs  18008  setcepi  18263  clatl  18682  ipopos  18710  psdmrn  18747  dirdm  18774  gsumress  18871  gsumvallem2  19030  gsumwspan  19042  trivsubgd  19363  trivsubgsnd  19364  trivnsgd  19382  cycsubg  19423  kerf1ghm  19461  conjnmz  19466  pmtrprfv  19667  symggen  19684  odf1o2  19787  gex1  19805  sylow2alem1  19831  smndlsmidm  19870  lsmss1  19879  lsmss2  19881  lsmmod  19889  lsmdisj  19895  lsmdisj2  19896  cntzcmn  20054  prmcyg  20108  dmdprdd  20215  dprdspan  20243  dprdres  20244  dprdz  20246  subgdmdprd  20250  subgdprd  20251  dprddisj2  20255  dprd2dlem1  20257  dprd2da  20258  dmdprdsplit2lem  20261  dprdsplit  20264  ablfacrp  20282  pgpfac1lem3  20293  isdrng4  20992  issubdrg  21037  lspun  21262  lspsn  21277  lspsnneg  21281  lsp0  21284  lsslsp  21290  lmhmlsp  21324  lspextmo  21331  lsmsp  21361  lspprabs  21370  lspsnvs  21392  lspdisj  21403  lsmcv  21419  lspsnat  21423  lsppratlem6  21430  lspprat  21431  lbsextlem4  21439  lidl1el  21505  0ringidl  21514  rspprop  21524  drngnidl  21531  lidldvgen  21658  cnsubrg  21733  mulgrhm2  21784  znrrg  21871  ocvin  21980  ocvlsp  21982  mrccss  22000  lindsenlbs  22157  topsn  23249  eltg4i  23278  unitg  23285  tgtop  23291  tgidm  23298  en2top  23303  basgen  23306  2basgen  23308  fctop  23322  cctop  23324  ppttop  23325  epttop  23327  ntrin  23379  isopn3  23384  opnnei  23438  neiuni  23440  maxlp  23465  clslp  23466  tgrest  23477  resttopon  23479  rest0  23487  restcls  23499  restntr  23500  ordtbas2  23509  ordtbas  23510  ordtrest2  23522  cmpcov2  23708  tgcmp  23719  cmpcld  23720  uncmp  23721  cmpfi  23726  dis2ndc  23779  restnlly  23801  dislly  23816  comppfsc  23851  kgentopon  23857  kgencmp  23864  kgenidm  23866  iskgen2  23867  kgencn3  23877  ptuni2  23895  ptbasfi  23900  xkouni  23918  txcls  23923  txdis  23951  txindis  23953  txcmplem2  23961  xkopt  23974  txconn  24008  qtopval2  24015  qtopuni  24021  qtoprest  24036  qtopomap  24037  qtopcmap  24038  kqsat  24050  kqcldsat  24052  hmeocls  24087  hmeontr  24088  hmphdis  24115  fgfil  24194  fgabs  24198  trfil1  24205  fgtr  24209  uzrest  24216  ufilmax  24226  ufileu  24238  filufint  24239  ufildom1  24245  rnelfm  24272  flimfil  24288  uffclsflim  24350  alexsublem  24363  alexsubALTlem3  24368  alexsubALT  24370  ptcmplem2  24372  ptcmplem3  24373  tgpconncompeqg  24431  haustsms2  24456  tgptsmscls  24469  ust0  24539  ustbas2  24544  iccntr  25141  pi1xfrcnv  25378  clsocv  25571  cfilfcls  25595  equivcmet  25638  hlhil  25764  evthicc2  25781  ovolshft  25832  volsup  25877  dyadmbllem  25920  mbfconstlem  25948  itg11  26012  limciun  26214  dvnres  26251  cpnord  26255  dvcmulf  26265  dvmptcmul  26284  dvcnvre  26339  plyco0  26510  taylthlem1  26700  taylthlem2  26701  ulmdvlem3  26729  wilthlem2  27396  ppisval  27431  ppinprm  27479  chtnprm  27481  ltsval2  28013  noextenddif  28025  cutsun12  28176  madebdaylemlrcut  28285  bdayiun  28301  cofcut1  28306  negbday  28443  oniso  28657  bdayons  28662  addonbday  28665  bdayn0p1  28755  plngrot  29268  upgrex  29670  uvtxnbgr  29981  cusgredg  30005  ubthlem1  31472  pjhth  31995  ococin  32010  chsupsn  32015  ssjo  32049  chabs1  32118  spansncvi  32254  mdslj1i  32921  mdslj2i  32922  atomli  32984  atcvatlem  32987  atcvat3i  32998  sumdmdlem  33020  difininv  33113  fnpreimac  33264  pmtrcnelor  33652  cycpmrn  33704  elrgspnlem4  33806  fldgenid  33881  1fldgenq  33884  rspidlid  33930  drngmxidl  34001  drngmxidlr  34002  esplyfvaln  34206  resssra  34219  dimkerim  34259  fldextrspunlem1  34307  fldextrspunlem2  34309  algextdeglem4  34352  cmpcref  34482  zarcls1  34501  zarclssn  34505  zart0  34511  zarcmplem  34513  xpinpreima2  34539  ordtrest2NEW  34555  sigagenid  34784  imambfm  34894  reprinfz1  35251  bnj1136  35627  bnj1398  35664  bnj1408  35666  bnj1498  35691  r1omhfb  35738  elscottrankeq  35746  fineqvacALT  35785  r1omhfbregs  35805  vonf1oonfo  35898  sconnpi1  36004  cvmliftlem15  36063  altopthsn  36726  nadddi  36973  opnbnd  37113  opnregcld  37118  cldregopn  37119  fnessref  37145  neibastop1  37147  topmeet  37152  topjoin  37153  fnemeet1  37154  fnejoin1  37156  ttctrid  37290  dfttc2g  37294  dfttc3gw  37311  bj-gabeqd  37850  bj-restpw  38013  bj-restb  38015  bj-restuni2  38019  dissneqlem  38263  pibt2  38340  poimirlem13  38551  poimirlem14  38552  poimirlem15  38553  fdc  38679  sstotbnd2  38708  isbnd2  38717  totbndbnd  38723  prdstotbnd  38728  heibor1  38744  1idl  38960  igenval2  39000  idreseqidinxp  39247  disjdmqs  39839  lshpdisj  40044  lssats  40069  lsatcvat3  40109  lshpset2N  40176  lfl1dim  40178  lfl1dim2N  40179  lkrpssN  40220  paddass  40895  paddidm  40898  pmod1i  40905  pmapjat1  40910  pclbtwnN  40954  pclunN  40955  paddunN  40984  pclfinclN  41007  dihjust  42274  dihmeetlem1N  42347  dihglblem5apreN  42348  dihmeetlem13N  42376  dochocsp  42436  dochdmj1  42447  dochnoncon  42448  dihjatb  42473  dihjat1lem  42485  lcfl9a  42562  lclkrlem2s  42582  lclkrlem2v  42585  mapdrvallem3  42703  mapdunirnN  42707  mapdin  42719  mapdlsm  42721  baerlem3lem2  42767  baerlem5alem2  42768  baerlem5blem2  42769  hdmaplkr  42970  primrootsunit1  43147  sticksstones11  43206  aks6d1c6lem5  43227  unitscyglem4  43248  rntrclfvOAI  43701  ismrcd1  43708  ismrcd2  43709  isnacs3  43720  nacsfix  43722  rgspnid  44169  iocinico  44213  onsupmaxb  44240  onsssupeqcond  44281  oacl2g  44331  omabs2  44333  omcl2  44334  ofoaf  44356  onsucunifi  44371  naddwordnexlem4  44402  harval3  44538  mptrcllem  44612  clcnvlem  44622  dmtrcl  44626  rntrcl  44627  cbviuneq12df  44660  dfrcl2  44673  dftrcl3  44719  brtrclfv2  44726  dfrtrcl3  44732  nzin  45301  iunincfi  46108  founiiun  46193  founiiun0  46204  inmap  46221  difmapsn  46224  funimaeq  46257  iuneqfzuz  46346  supminfrnmpt  46454  supminfxr2  46478  supminfxrrnmpt  46480  pimxrneun  46497  iooiinicc  46553  icomnfinre  46563  iooiinioc  46567  limsupresxr  46775  liminfresxr  46776  limsup10exlem  46781  liminfvalxr  46792  fourierdlem79  47194  rrxsnicc  47309  prsal  47327  issalgend  47347  sge0f1o  47391  caragenuni  47520  caragendifcl  47523  opnvonmbllem2  47642  iinhoiicc  47683  pimconstlt1  47711  pimltpnff  47712  pimiooltgt  47719  pimgtmnf2  47723  pimdecfgtioc  47724  pimincfltioc  47725  pimdecfgtioo  47726  pimincfltioo  47727  preimageiingt  47729  preimaleiinlt  47730  pimgtmnff  47731  sssmf  47747  smflimlem5  47784  smfmullem4  47803  smfpimbor1lem2  47808  smfsuplem1  47820  smfpimne2  47849  fsupdm  47851  finfdm  47855  tmachlem-agreesn  47956  sprsymrelf1  48577  lspeqlco  49550  iunlub  49930  iinglb  49931  iuneqconst2  49932  iineqconst2  49933  isclatd  50090  intubeu  50091  unilbeu  50092  setrecsres  50794