Theorem eqssd 4026

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  eqelssd  4030  uneqdifeq  4516  pweq  4636  unieq  4942  unissel  4962  intmin  4992  unissint  4996  int0el  5003  intidg  5477  dmcosseq  5999  dmcosseqOLD  6000  sofld  6218  relfld  6306  preddowncl  6364  frpoind  6374  wfiOLD  6383  tz7.7  6421  fimacnvOLD  7104  knatar  7393  sorpssuni  7767  sorpssint  7768  onint  7826  fo2ndf  8162  suppimacnv  8215  tposeq  8269  frrlem14  8340  onfununi  8397  tfrlem15  8448  oaass  8617  odi  8635  omass  8636  oelim2  8651  oeeui  8658  nnawordex  8693  oaabslem  8703  oaabs2  8705  omabslem  8706  omabs  8707  cofon1  8728  uniinqs  8855  sucdom2OLD  9148  sucdom2  9269  onomeneq  9291  fineqv  9326  dffi2  9492  fiuni  9497  dffi3  9500  hartogslem1  9611  ixpiunwdom  9659  cantnfp1lem3  9749  oemapvali  9753  cantnf  9762  dfttrcl2  9793  frind  9819  r1val1  9855  rankval3b  9895  rankunb  9919  rankuni2b  9922  rankr1id  9931  rankc2  9940  rankxplim  9948  tcrank  9953  carden2b  10036  harval2  10066  en2other2  10078  infpwfien  10131  coflim  10330  cfcof  10343  cfidm  10344  isf32lem2  10423  fin1a2lem11  10479  fin1a2lem13  10481  ttukeylem7  10584  fpwwe2  10712  winafp  10766  wuncidm  10815  wuncval2  10816  tskuni  10852  grur1  10889  distrpr  11097  ltexpri  11112  reclem4pr  11119  fzopth  13621  fzosplit  13749  fzouzsplit  13751  fzoopth  13812  ccatrn  14637  cotrtrclfv  15061  dmtrclfv  15067  dfrtrcl2  15111  structcnvcnv  17200  imasaddfnlem  17588  imasvscafn  17597  mrcuni  17679  mressmrcd  17685  submrc  17686  ssceq  17887  rescabs  17896  rescabsOLD  17897  setcepi  18155  clatl  18578  ipopos  18606  psdmrn  18643  dirdm  18670  gsumress  18720  gsumvallem2  18869  gsumwspan  18881  trivsubgd  19193  trivsubgsnd  19194  trivnsgd  19212  cycsubg  19248  kerf1ghm  19287  conjnmz  19292  pmtrprfv  19495  symggen  19512  odf1o2  19615  gex1  19633  sylow2alem1  19659  smndlsmidm  19698  lsmss1  19707  lsmss2  19709  lsmmod  19717  lsmdisj  19723  lsmdisj2  19724  cntzcmn  19882  prmcyg  19936  dmdprdd  20043  dprdspan  20071  dprdres  20072  dprdz  20074  subgdmdprd  20078  subgdprd  20079  dprddisj2  20083  dprd2dlem1  20085  dprd2da  20086  dmdprdsplit2lem  20089  dprdsplit  20092  ablfacrp  20110  pgpfac1lem3  20121  issubdrg  20803  lspun  21008  lspsn  21023  lspsnneg  21027  lsp0  21030  lsslsp  21036  lsslspOLD  21037  lmhmlsp  21071  lspextmo  21078  lsmsp  21108  lspprabs  21117  lspsnvs  21139  lspdisj  21150  lsmcv  21166  lspsnat  21170  lsppratlem6  21177  lspprat  21178  lbsextlem4  21186  lidl1el  21259  drngnidl  21276  lidldvgen  21367  cnsubrg  21468  mulgrhm2  21512  znrrg  21607  ocvin  21715  ocvlsp  21717  mrccss  21735  topsn  22958  eltg4i  22988  unitg  22995  tgtop  23001  tgidm  23008  en2top  23013  basgen  23016  2basgen  23018  fctop  23032  cctop  23034  ppttop  23035  epttop  23037  ntrin  23090  isopn3  23095  opnnei  23149  neiuni  23151  maxlp  23176  clslp  23177  tgrest  23188  resttopon  23190  rest0  23198  restcls  23210  restntr  23211  ordtbas2  23220  ordtbas  23221  ordtrest2  23233  cmpcov2  23419  tgcmp  23430  cmpcld  23431  uncmp  23432  cmpfi  23437  dis2ndc  23489  restnlly  23511  dislly  23526  comppfsc  23561  kgentopon  23567  kgencmp  23574  kgenidm  23576  iskgen2  23577  kgencn3  23587  ptuni2  23605  ptbasfi  23610  xkouni  23628  txcls  23633  txdis  23661  txindis  23663  txcmplem2  23671  xkopt  23684  txconn  23718  qtopval2  23725  qtopuni  23731  qtoprest  23746  qtopomap  23747  qtopcmap  23748  kqsat  23760  kqcldsat  23762  hmeocls  23797  hmeontr  23798  hmphdis  23825  fgfil  23904  fgabs  23908  trfil1  23915  fgtr  23919  uzrest  23926  ufilmax  23936  ufileu  23948  filufint  23949  ufildom1  23955  rnelfm  23982  flimfil  23998  uffclsflim  24060  alexsublem  24073  alexsubALTlem3  24078  alexsubALT  24080  ptcmplem2  24082  ptcmplem3  24083  tgpconncompeqg  24141  haustsms2  24166  tgptsmscls  24179  ust0  24249  ustbas2  24255  iccntr  24862  pi1xfrcnv  25109  clsocv  25303  cfilfcls  25327  equivcmet  25370  hlhil  25496  evthicc2  25514  ovolshft  25565  volsup  25610  dyadmbllem  25653  mbfconstlem  25681  itg11  25745  limciun  25949  dvnres  25987  cpnord  25991  dvcmulf  26002  dvmptcmul  26022  dvcnvre  26078  plyco0  26251  taylthlem1  26433  taylthlem2  26434  taylthlem2OLD  26435  ulmdvlem3  26463  wilthlem2  27130  ppisval  27165  ppinprm  27213  chtnprm  27215  sltval2  27719  noextenddif  27731  scutun12  27873  madebdaylemlrcut  27955  cofcut1  27972  negsbday  28107  upgrex  29127  uvtxnbgr  29435  cusgredg  29459  ubthlem1  30902  pjhth  31425  ococin  31440  chsupsn  31445  ssjo  31479  chabs1  31548  spansncvi  31684  mdslj1i  32351  mdslj2i  32352  atomli  32414  atcvatlem  32417  atcvat3i  32428  sumdmdlem  32450  difininv  32547  fnpreimac  32689  pmtrcnelor  33084  cycpmrn  33136  isdrng4  33264  fldgenid  33286  1fldgenq  33289  rspidlid  33368  0ringidl  33414  drngmxidl  33470  drngmxidlr  33471  resssra  33602  dimkerim  33640  algextdeglem4  33711  cmpcref  33796  zarcls1  33815  zarclssn  33819  zart0  33825  zarcmplem  33827  xpinpreima2  33853  ordtrest2NEW  33869  sigagenid  34115  imambfm  34227  reprinfz1  34599  bnj1136  34973  bnj1398  35010  bnj1408  35012  bnj1498  35037  fineqvacALT  35074  sconnpi1  35207  cvmliftlem15  35266  altopthsn  35925  opnbnd  36291  opnregcld  36296  cldregopn  36297  fnessref  36323  neibastop1  36325  topmeet  36330  topjoin  36331  fnemeet1  36332  fnejoin1  36334  bj-gabeqd  36903  bj-restpw  37058  bj-restb  37060  bj-restuni2  37064  dissneqlem  37306  pibt2  37383  lindsenlbs  37575  poimirlem13  37593  poimirlem14  37594  poimirlem15  37595  fdc  37705  sstotbnd2  37734  isbnd2  37743  totbndbnd  37749  prdstotbnd  37754  heibor1  37770  1idl  37986  igenval2  38026  idreseqidinxp  38265  disjdmqs  38760  lshpdisj  38943  lssats  38968  lsatcvat3  39008  lshpset2N  39075  lfl1dim  39077  lfl1dim2N  39078  lkrpssN  39119  paddass  39795  paddidm  39798  pmod1i  39805  pmapjat1  39810  pclbtwnN  39854  pclunN  39855  paddunN  39884  pclfinclN  39907  dihjust  41174  dihmeetlem1N  41247  dihglblem5apreN  41248  dihmeetlem13N  41276  dochocsp  41336  dochdmj1  41347  dochnoncon  41348  dihjatb  41373  dihjat1lem  41385  lcfl9a  41462  lclkrlem2s  41482  lclkrlem2v  41485  mapdrvallem3  41603  mapdunirnN  41607  mapdin  41619  mapdlsm  41621  baerlem3lem2  41667  baerlem5alem2  41668  baerlem5blem2  41669  hdmaplkr  41870  primrootsunit1  42054  sticksstones11  42113  aks6d1c6lem5  42134  unitscyglem4  42155  rntrclfvOAI  42647  ismrcd1  42654  ismrcd2  42655  isnacs3  42666  nacsfix  42668  rgspnid  43129  iocinico  43173  onsupmaxb  43200  onsssupeqcond  43242  oacl2g  43292  omabs2  43294  omcl2  43295  ofoaf  43317  onsucunifi  43332  naddwordnexlem4  43363  harval3  43500  mptrcllem  43575  clcnvlem  43585  dmtrcl  43589  rntrcl  43590  cbviuneq12df  43623  dfrcl2  43636  dftrcl3  43682  brtrclfv2  43689  dfrtrcl3  43695  scottrankd  44217  nzin  44287  iunincfi  44996  founiiun  45086  founiiun0  45097  inmap  45116  difmapsn  45119  funimaeq  45155  iuneqfzuz  45250  supminfrnmpt  45360  supminfxr2  45384  supminfxrrnmpt  45386  pimxrneun  45404  iooiinicc  45460  icomnfinre  45470  iooiinioc  45474  limsupresxr  45687  liminfresxr  45688  limsup10exlem  45693  liminfvalxr  45704  fourierdlem79  46106  rrxsnicc  46221  prsal  46239  issalgend  46259  sge0f1o  46303  caragenuni  46432  caragendifcl  46435  opnvonmbllem2  46554  iinhoiicc  46595  pimconstlt1  46623  pimltpnff  46624  pimiooltgt  46631  pimgtmnf2  46635  pimdecfgtioc  46636  pimincfltioc  46637  pimdecfgtioo  46638  pimincfltioo  46639  preimageiingt  46641  preimaleiinlt  46642  pimgtmnff  46643  sssmf  46659  smflimlem5  46696  smfmullem4  46715  smfpimbor1lem2  46720  smfsuplem1  46732  smfpimne2  46761  fsupdm  46763  finfdm  46767  sprsymrelf1  47370  lspeqlco  48168  isclatd  48655  intubeu  48656  unilbeu  48657  setrecsres  48794