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  4440  pweq  4561  unieq  4867  unissel  4888  intmin  4916  unissint  4920  int0el  4927  intidg  5396  dmcosseq  5916  dmcosseqOLD  5917  dmcosseqOLDOLD  5918  imadifssran  6098  sofld  6134  relfld  6222  preddowncl  6279  frpoind  6289  tz7.7  6332  f1imadifssran  6567  knatar  7291  sorpssuni  7665  sorpssint  7666  onint  7723  fo2ndf  8051  suppimacnv  8104  tposeq  8158  frrlem14  8229  onfununi  8261  tfrlem15  8311  oaass  8476  odi  8494  omass  8495  oelim2  8510  oeeui  8517  nnawordex  8552  oaabslem  8562  oaabs2  8564  omabslem  8565  omabs  8566  cofon1  8587  uniinqs  8721  sucdom2  9112  onomeneq  9123  fineqv  9151  dffi2  9307  fiuni  9312  dffi3  9315  hartogslem1  9428  ixpiunwdom  9476  cantnfp1lem3  9570  oemapvali  9574  cantnf  9583  dfttrcl2  9614  frind  9643  r1val1  9679  rankval3b  9719  rankunb  9743  rankuni2b  9746  rankr1id  9755  rankc2  9764  rankxplim  9772  tcrank  9777  carden2b  9860  harval2  9890  en2other2  9900  infpwfien  9953  coflim  10152  cfcof  10165  cfidm  10166  isf32lem2  10245  fin1a2lem11  10301  fin1a2lem13  10303  ttukeylem7  10406  fpwwe2  10534  winafp  10588  wuncidm  10637  wuncval2  10638  tskuni  10674  grur1  10711  distrpr  10919  ltexpri  10934  reclem4pr  10941  fzopth  13461  fzosplit  13592  fzouzsplit  13594  fzoopth  13662  ccatrn  14497  cotrtrclfv  14919  dmtrclfv  14925  dfrtrcl2  14969  structcnvcnv  17064  imasaddfnlem  17432  imasvscafn  17441  mrcuni  17527  mressmrcd  17533  submrc  17534  ssceq  17733  rescabs  17740  setcepi  17995  clatl  18414  ipopos  18442  psdmrn  18479  dirdm  18506  gsumress  18590  gsumvallem2  18742  gsumwspan  18754  trivsubgd  19065  trivsubgsnd  19066  trivnsgd  19084  cycsubg  19120  kerf1ghm  19159  conjnmz  19164  pmtrprfv  19365  symggen  19382  odf1o2  19485  gex1  19503  sylow2alem1  19529  smndlsmidm  19568  lsmss1  19577  lsmss2  19579  lsmmod  19587  lsmdisj  19593  lsmdisj2  19594  cntzcmn  19752  prmcyg  19806  dmdprdd  19913  dprdspan  19941  dprdres  19942  dprdz  19944  subgdmdprd  19948  subgdprd  19949  dprddisj2  19953  dprd2dlem1  19955  dprd2da  19956  dmdprdsplit2lem  19959  dprdsplit  19962  ablfacrp  19980  pgpfac1lem3  19991  issubdrg  20695  lspun  20920  lspsn  20935  lspsnneg  20939  lsp0  20942  lsslsp  20948  lsslspOLD  20949  lmhmlsp  20983  lspextmo  20990  lsmsp  21020  lspprabs  21029  lspsnvs  21051  lspdisj  21062  lsmcv  21078  lspsnat  21082  lsppratlem6  21089  lspprat  21090  lbsextlem4  21098  lidl1el  21163  drngnidl  21180  lidldvgen  21271  cnsubrg  21364  mulgrhm2  21415  znrrg  21502  ocvin  21611  ocvlsp  21613  mrccss  21631  topsn  22846  eltg4i  22875  unitg  22882  tgtop  22888  tgidm  22895  en2top  22900  basgen  22903  2basgen  22905  fctop  22919  cctop  22921  ppttop  22922  epttop  22924  ntrin  22976  isopn3  22981  opnnei  23035  neiuni  23037  maxlp  23062  clslp  23063  tgrest  23074  resttopon  23076  rest0  23084  restcls  23096  restntr  23097  ordtbas2  23106  ordtbas  23107  ordtrest2  23119  cmpcov2  23305  tgcmp  23316  cmpcld  23317  uncmp  23318  cmpfi  23323  dis2ndc  23375  restnlly  23397  dislly  23412  comppfsc  23447  kgentopon  23453  kgencmp  23460  kgenidm  23462  iskgen2  23463  kgencn3  23473  ptuni2  23491  ptbasfi  23496  xkouni  23514  txcls  23519  txdis  23547  txindis  23549  txcmplem2  23557  xkopt  23570  txconn  23604  qtopval2  23611  qtopuni  23617  qtoprest  23632  qtopomap  23633  qtopcmap  23634  kqsat  23646  kqcldsat  23648  hmeocls  23683  hmeontr  23684  hmphdis  23711  fgfil  23790  fgabs  23794  trfil1  23801  fgtr  23805  uzrest  23812  ufilmax  23822  ufileu  23834  filufint  23835  ufildom1  23841  rnelfm  23868  flimfil  23884  uffclsflim  23946  alexsublem  23959  alexsubALTlem3  23964  alexsubALT  23966  ptcmplem2  23968  ptcmplem3  23969  tgpconncompeqg  24027  haustsms2  24052  tgptsmscls  24065  ust0  24135  ustbas2  24140  iccntr  24737  pi1xfrcnv  24984  clsocv  25177  cfilfcls  25201  equivcmet  25244  hlhil  25370  evthicc2  25388  ovolshft  25439  volsup  25484  dyadmbllem  25527  mbfconstlem  25555  itg11  25619  limciun  25822  dvnres  25860  cpnord  25864  dvcmulf  25875  dvmptcmul  25895  dvcnvre  25951  plyco0  26124  taylthlem1  26308  taylthlem2  26309  taylthlem2OLD  26310  ulmdvlem3  26338  wilthlem2  27006  ppisval  27041  ppinprm  27089  chtnprm  27091  sltval2  27595  noextenddif  27607  scutun12  27751  madebdaylemlrcut  27844  bdayiun  27860  cofcut1  27864  negsbday  27999  onsiso  28205  bdayon  28209  bdayn0p1  28294  upgrex  29070  uvtxnbgr  29378  cusgredg  29402  ubthlem1  30850  pjhth  31373  ococin  31388  chsupsn  31393  ssjo  31427  chabs1  31496  spansncvi  31632  mdslj1i  32299  mdslj2i  32300  atomli  32362  atcvatlem  32365  atcvat3i  32376  sumdmdlem  32398  difininv  32497  fnpreimac  32653  pmtrcnelor  33060  cycpmrn  33112  elrgspnlem4  33212  isdrng4  33261  fldgenid  33285  1fldgenq  33288  rspidlid  33340  0ringidl  33386  drngmxidl  33442  drngmxidlr  33443  resssra  33599  dimkerim  33640  fldextrspunlem1  33688  fldextrspunlem2  33690  algextdeglem4  33733  cmpcref  33863  zarcls1  33882  zarclssn  33886  zart0  33892  zarcmplem  33894  xpinpreima2  33920  ordtrest2NEW  33936  sigagenid  34164  imambfm  34275  reprinfz1  34635  bnj1136  35009  bnj1398  35046  bnj1408  35048  bnj1498  35073  rankval4b  35111  r1omhfb  35123  r1omhfbregs  35133  fineqvacALT  35140  sconnpi1  35283  cvmliftlem15  35342  altopthsn  36005  opnbnd  36369  opnregcld  36374  cldregopn  36375  fnessref  36401  neibastop1  36403  topmeet  36408  topjoin  36409  fnemeet1  36410  fnejoin1  36412  bj-gabeqd  36981  bj-restpw  37136  bj-restb  37138  bj-restuni2  37142  dissneqlem  37384  pibt2  37461  lindsenlbs  37665  poimirlem13  37683  poimirlem14  37684  poimirlem15  37685  fdc  37795  sstotbnd2  37824  isbnd2  37833  totbndbnd  37839  prdstotbnd  37844  heibor1  37860  1idl  38076  igenval2  38116  idreseqidinxp  38357  disjdmqs  38912  lshpdisj  39096  lssats  39121  lsatcvat3  39161  lshpset2N  39228  lfl1dim  39230  lfl1dim2N  39231  lkrpssN  39272  paddass  39947  paddidm  39950  pmod1i  39957  pmapjat1  39962  pclbtwnN  40006  pclunN  40007  paddunN  40036  pclfinclN  40059  dihjust  41326  dihmeetlem1N  41399  dihglblem5apreN  41400  dihmeetlem13N  41428  dochocsp  41488  dochdmj1  41499  dochnoncon  41500  dihjatb  41525  dihjat1lem  41537  lcfl9a  41614  lclkrlem2s  41634  lclkrlem2v  41637  mapdrvallem3  41755  mapdunirnN  41759  mapdin  41771  mapdlsm  41773  baerlem3lem2  41819  baerlem5alem2  41820  baerlem5blem2  41821  hdmaplkr  42022  primrootsunit1  42200  sticksstones11  42259  aks6d1c6lem5  42280  unitscyglem4  42301  rntrclfvOAI  42794  ismrcd1  42801  ismrcd2  42802  isnacs3  42813  nacsfix  42815  rgspnid  43271  iocinico  43315  onsupmaxb  43342  onsssupeqcond  43383  oacl2g  43433  omabs2  43435  omcl2  43436  ofoaf  43458  onsucunifi  43473  naddwordnexlem4  43504  harval3  43641  mptrcllem  43716  clcnvlem  43726  dmtrcl  43730  rntrcl  43731  cbviuneq12df  43764  dfrcl2  43777  dftrcl3  43823  brtrclfv2  43830  dfrtrcl3  43836  scottrankd  44351  nzin  44421  iunincfi  45201  founiiun  45286  founiiun0  45297  inmap  45316  difmapsn  45319  funimaeq  45353  iuneqfzuz  45444  supminfrnmpt  45553  supminfxr2  45577  supminfxrrnmpt  45579  pimxrneun  45596  iooiinicc  45652  icomnfinre  45662  iooiinioc  45666  limsupresxr  45874  liminfresxr  45875  limsup10exlem  45880  liminfvalxr  45891  fourierdlem79  46293  rrxsnicc  46408  prsal  46426  issalgend  46446  sge0f1o  46490  caragenuni  46619  caragendifcl  46622  opnvonmbllem2  46741  iinhoiicc  46782  pimconstlt1  46810  pimltpnff  46811  pimiooltgt  46818  pimgtmnf2  46822  pimdecfgtioc  46823  pimincfltioc  46824  pimdecfgtioo  46825  pimincfltioo  46826  preimageiingt  46828  preimaleiinlt  46829  pimgtmnff  46830  sssmf  46846  smflimlem5  46883  smfmullem4  46902  smfpimbor1lem2  46907  smfsuplem1  46919  smfpimne2  46948  fsupdm  46950  finfdm  46954  sprsymrelf1  47606  lspeqlco  48550  iunlub  48931  iinglb  48932  iuneqconst2  48933  iineqconst2  48934  isclatd  49093  intubeu  49094  unilbeu  49095  setrecsres  49813