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 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  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  5432  dmcosseq  5962  dmcosseqOLD  5963  sofld  6180  imadifssran  6197  imadifssranOLD  6198  relfld  6272  preddowncl  6330  frpoind  6340  tz7.7  6383  knatar  7360  sorpssuni  7733  sorpssint  7734  onint  7789  fo2ndf  8118  suppimacnv  8172  tposeq  8226  frrlem14  8298  onfununi  8330  tfrlem15  8381  oaass  8548  odi  8566  omass  8567  oelim2  8583  oeeui  8590  nnawordex  8625  oaabslem  8635  oaabs2  8637  omabslem  8638  omabs  8639  cofon1  8660  uniinqs  8797  sucdom2  9197  onomeneq  9208  fineqv  9237  dffi2  9393  fiuni  9398  dffi3  9401  hartogslem1  9514  ixpiunwdom  9562  cantnfp1lem3  9659  oemapvali  9663  cantnf  9672  dfttrcl2  9703  frind  9732  r1val1  9768  rankval3b  9808  rankunb  9832  rankuni2b  9835  rankr1id  9844  rankc2  9853  rankxplim  9861  tcrank  9866  scottrankd  9888  carden2b  9972  harval2  10002  en2other2  10012  infpwfien  10065  coflim  10263  cfcof  10276  cfidm  10277  isf32lem2  10356  fin1a2lem11  10412  fin1a2lem13  10414  ttukeylem7  10517  fpwwe2  10652  winafp  10706  wuncidm  10755  wuncval2  10756  tskuni  10792  grur1  10829  distrpr  11037  ltexpri  11052  reclem4pr  11059  fzopth  13616  fzosplit  13748  fzouzsplit  13750  fzoopth  13818  ccatrn  14655  cotrtrclfv  15085  dmtrclfv  15091  dfrtrcl2  15135  structcnvcnv  17245  imasaddfnlem  17614  imasvscafn  17623  mrcuni  17709  mressmrcd  17715  submrc  17716  ssceq  17915  rescabs  17922  setcepi  18177  clatl  18596  ipopos  18624  psdmrn  18661  dirdm  18688  gsumress  18784  gsumvallem2  18943  gsumwspan  18955  trivsubgd  19276  trivsubgsnd  19277  trivnsgd  19295  cycsubg  19336  kerf1ghm  19374  conjnmz  19379  pmtrprfv  19580  symggen  19597  odf1o2  19700  gex1  19718  sylow2alem1  19744  smndlsmidm  19783  lsmss1  19792  lsmss2  19794  lsmmod  19802  lsmdisj  19808  lsmdisj2  19809  cntzcmn  19967  prmcyg  20021  dmdprdd  20128  dprdspan  20156  dprdres  20157  dprdz  20159  subgdmdprd  20163  subgdprd  20164  dprddisj2  20168  dprd2dlem1  20170  dprd2da  20171  dmdprdsplit2lem  20174  dprdsplit  20177  ablfacrp  20195  pgpfac1lem3  20206  isdrng4  20902  issubdrg  20946  lspun  21171  lspsn  21186  lspsnneg  21190  lsp0  21193  lsslsp  21199  lmhmlsp  21233  lspextmo  21240  lsmsp  21270  lspprabs  21279  lspsnvs  21301  lspdisj  21312  lsmcv  21328  lspsnat  21332  lsppratlem6  21339  lspprat  21340  lbsextlem4  21348  lidl1el  21414  0ringidl  21423  rspprop  21433  drngnidl  21440  lidldvgen  21565  cnsubrg  21640  mulgrhm2  21691  znrrg  21778  ocvin  21887  ocvlsp  21889  mrccss  21907  lindsenlbs  22064  topsn  23156  eltg4i  23185  unitg  23192  tgtop  23198  tgidm  23205  en2top  23210  basgen  23213  2basgen  23215  fctop  23229  cctop  23231  ppttop  23232  epttop  23234  ntrin  23286  isopn3  23291  opnnei  23345  neiuni  23347  maxlp  23372  clslp  23373  tgrest  23384  resttopon  23386  rest0  23394  restcls  23406  restntr  23407  ordtbas2  23416  ordtbas  23417  ordtrest2  23429  cmpcov2  23615  tgcmp  23626  cmpcld  23627  uncmp  23628  cmpfi  23633  dis2ndc  23686  restnlly  23708  dislly  23723  comppfsc  23758  kgentopon  23764  kgencmp  23771  kgenidm  23773  iskgen2  23774  kgencn3  23784  ptuni2  23802  ptbasfi  23807  xkouni  23825  txcls  23830  txdis  23858  txindis  23860  txcmplem2  23868  xkopt  23881  txconn  23915  qtopval2  23922  qtopuni  23928  qtoprest  23943  qtopomap  23944  qtopcmap  23945  kqsat  23957  kqcldsat  23959  hmeocls  23994  hmeontr  23995  hmphdis  24022  fgfil  24101  fgabs  24105  trfil1  24112  fgtr  24116  uzrest  24123  ufilmax  24133  ufileu  24145  filufint  24146  ufildom1  24152  rnelfm  24179  flimfil  24195  uffclsflim  24257  alexsublem  24270  alexsubALTlem3  24275  alexsubALT  24277  ptcmplem2  24279  ptcmplem3  24280  tgpconncompeqg  24338  haustsms2  24363  tgptsmscls  24376  ust0  24446  ustbas2  24451  iccntr  25048  pi1xfrcnv  25285  clsocv  25478  cfilfcls  25502  equivcmet  25545  hlhil  25671  evthicc2  25688  ovolshft  25739  volsup  25784  dyadmbllem  25827  mbfconstlem  25855  itg11  25919  limciun  26121  dvnres  26158  cpnord  26162  dvcmulf  26172  dvmptcmul  26191  dvcnvre  26246  plyco0  26417  taylthlem1  26609  taylthlem2  26610  ulmdvlem3  26638  wilthlem2  27305  ppisval  27340  ppinprm  27388  chtnprm  27390  ltsval2  27892  noextenddif  27904  cutsun12  28055  madebdaylemlrcut  28164  bdayiun  28180  cofcut1  28185  negbday  28322  oniso  28536  bdayons  28541  addonbday  28544  bdayn0p1  28634  plngrot  29147  upgrex  29549  uvtxnbgr  29860  cusgredg  29884  ubthlem1  31351  pjhth  31874  ococin  31889  chsupsn  31894  ssjo  31928  chabs1  31997  spansncvi  32133  mdslj1i  32800  mdslj2i  32801  atomli  32863  atcvatlem  32866  atcvat3i  32877  sumdmdlem  32899  difininv  32992  fnpreimac  33143  pmtrcnelor  33531  cycpmrn  33583  elrgspnlem4  33685  fldgenid  33760  1fldgenq  33763  rspidlid  33809  drngmxidl  33879  drngmxidlr  33880  esplyfvaln  34084  resssra  34097  dimkerim  34137  fldextrspunlem1  34185  fldextrspunlem2  34187  algextdeglem4  34230  cmpcref  34360  zarcls1  34379  zarclssn  34383  zart0  34389  zarcmplem  34391  xpinpreima2  34417  ordtrest2NEW  34433  sigagenid  34662  imambfm  34773  reprinfz1  35130  bnj1136  35506  bnj1398  35543  bnj1408  35545  bnj1498  35570  rankval4b  35607  r1omhfb  35622  elscottrankeq  35629  fineqvacALT  35643  r1omhfbregs  35663  vonf1oonfo  35712  sconnpi1  35818  cvmliftlem15  35877  altopthsn  36541  nadddi  36804  opnbnd  36944  opnregcld  36949  cldregopn  36950  fnessref  36976  neibastop1  36978  topmeet  36983  topjoin  36984  fnemeet1  36985  fnejoin1  36987  ttctrid  37121  dfttc2g  37125  dfttc3gw  37142  bj-gabeqd  37681  bj-restpw  37842  bj-restb  37844  bj-restuni2  37848  dissneqlem  38094  pibt2  38171  poimirlem13  38382  poimirlem14  38383  poimirlem15  38384  fdc  38495  sstotbnd2  38524  isbnd2  38533  totbndbnd  38539  prdstotbnd  38544  heibor1  38560  1idl  38776  igenval2  38816  idreseqidinxp  39063  disjdmqs  39655  lshpdisj  39860  lssats  39885  lsatcvat3  39925  lshpset2N  39992  lfl1dim  39994  lfl1dim2N  39995  lkrpssN  40036  paddass  40711  paddidm  40714  pmod1i  40721  pmapjat1  40726  pclbtwnN  40770  pclunN  40771  paddunN  40800  pclfinclN  40823  dihjust  42090  dihmeetlem1N  42163  dihglblem5apreN  42164  dihmeetlem13N  42192  dochocsp  42252  dochdmj1  42263  dochnoncon  42264  dihjatb  42289  dihjat1lem  42301  lcfl9a  42378  lclkrlem2s  42398  lclkrlem2v  42401  mapdrvallem3  42519  mapdunirnN  42523  mapdin  42535  mapdlsm  42537  baerlem3lem2  42583  baerlem5alem2  42584  baerlem5blem2  42585  hdmaplkr  42786  primrootsunit1  42963  sticksstones11  43022  aks6d1c6lem5  43043  unitscyglem4  43064  rntrclfvOAI  43536  ismrcd1  43543  ismrcd2  43544  isnacs3  43555  nacsfix  43557  rgspnid  44009  iocinico  44053  onsupmaxb  44080  onsssupeqcond  44121  oacl2g  44171  omabs2  44173  omcl2  44174  ofoaf  44196  onsucunifi  44211  naddwordnexlem4  44242  harval3  44378  mptrcllem  44453  clcnvlem  44463  dmtrcl  44467  rntrcl  44468  cbviuneq12df  44501  dfrcl2  44514  dftrcl3  44560  brtrclfv2  44567  dfrtrcl3  44573  nzin  45142  iunincfi  45926  founiiun  46011  founiiun0  46022  inmap  46039  difmapsn  46042  funimaeq  46075  iuneqfzuz  46165  supminfrnmpt  46273  supminfxr2  46297  supminfxrrnmpt  46299  pimxrneun  46316  iooiinicc  46372  icomnfinre  46382  iooiinioc  46386  limsupresxr  46594  liminfresxr  46595  limsup10exlem  46600  liminfvalxr  46611  fourierdlem79  47013  rrxsnicc  47128  prsal  47146  issalgend  47166  sge0f1o  47210  caragenuni  47339  caragendifcl  47342  opnvonmbllem2  47461  iinhoiicc  47502  pimconstlt1  47530  pimltpnff  47531  pimiooltgt  47538  pimgtmnf2  47542  pimdecfgtioc  47543  pimincfltioc  47544  pimdecfgtioo  47545  pimincfltioo  47546  preimageiingt  47548  preimaleiinlt  47549  pimgtmnff  47550  sssmf  47566  smflimlem5  47603  smfmullem4  47622  smfpimbor1lem2  47627  smfsuplem1  47639  smfpimne2  47668  fsupdm  47670  finfdm  47674  tmachlem-agreesn  47775  sprsymrelf1  48396  lspeqlco  49369  iunlub  49749  iinglb  49750  iuneqconst2  49751  iineqconst2  49752  isclatd  49909  intubeu  49910  unilbeu  49911  setrecsres  50628