Theorem eqssd 3964

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3931

This theorem is referenced by:  eqelssd  3968  uneqdifeq  4456  pweq  4577  unieq  4882  unissel  4902  intmin  4932  unissint  4936  int0el  4943  intidg  5417  dmcosseq  5940  dmcosseqOLD  5941  imadifssran  6124  sofld  6160  relfld  6248  preddowncl  6305  frpoind  6315  tz7.7  6358  f1imadifssran  6602  knatar  7332  sorpssuni  7708  sorpssint  7709  onint  7766  fo2ndf  8100  suppimacnv  8153  tposeq  8207  frrlem14  8278  onfununi  8310  tfrlem15  8360  oaass  8525  odi  8543  omass  8544  oelim2  8559  oeeui  8566  nnawordex  8601  oaabslem  8611  oaabs2  8613  omabslem  8614  omabs  8615  cofon1  8636  uniinqs  8770  sucdom2  9167  onomeneq  9178  fineqv  9210  dffi2  9374  fiuni  9379  dffi3  9382  hartogslem1  9495  ixpiunwdom  9543  cantnfp1lem3  9633  oemapvali  9637  cantnf  9646  dfttrcl2  9677  frind  9703  r1val1  9739  rankval3b  9779  rankunb  9803  rankuni2b  9806  rankr1id  9815  rankc2  9824  rankxplim  9832  tcrank  9837  carden2b  9920  harval2  9950  en2other2  9962  infpwfien  10015  coflim  10214  cfcof  10227  cfidm  10228  isf32lem2  10307  fin1a2lem11  10363  fin1a2lem13  10365  ttukeylem7  10468  fpwwe2  10596  winafp  10650  wuncidm  10699  wuncval2  10700  tskuni  10736  grur1  10773  distrpr  10981  ltexpri  10996  reclem4pr  11003  fzopth  13522  fzosplit  13653  fzouzsplit  13655  fzoopth  13723  ccatrn  14554  cotrtrclfv  14978  dmtrclfv  14984  dfrtrcl2  15028  structcnvcnv  17123  imasaddfnlem  17491  imasvscafn  17500  mrcuni  17582  mressmrcd  17588  submrc  17589  ssceq  17788  rescabs  17795  setcepi  18050  clatl  18467  ipopos  18495  psdmrn  18532  dirdm  18559  gsumress  18609  gsumvallem2  18761  gsumwspan  18773  trivsubgd  19085  trivsubgsnd  19086  trivnsgd  19104  cycsubg  19140  kerf1ghm  19179  conjnmz  19184  pmtrprfv  19383  symggen  19400  odf1o2  19503  gex1  19521  sylow2alem1  19547  smndlsmidm  19586  lsmss1  19595  lsmss2  19597  lsmmod  19605  lsmdisj  19611  lsmdisj2  19612  cntzcmn  19770  prmcyg  19824  dmdprdd  19931  dprdspan  19959  dprdres  19960  dprdz  19962  subgdmdprd  19966  subgdprd  19967  dprddisj2  19971  dprd2dlem1  19973  dprd2da  19974  dmdprdsplit2lem  19977  dprdsplit  19980  ablfacrp  19998  pgpfac1lem3  20009  issubdrg  20689  lspun  20893  lspsn  20908  lspsnneg  20912  lsp0  20915  lsslsp  20921  lsslspOLD  20922  lmhmlsp  20956  lspextmo  20963  lsmsp  20993  lspprabs  21002  lspsnvs  21024  lspdisj  21035  lsmcv  21051  lspsnat  21055  lsppratlem6  21062  lspprat  21063  lbsextlem4  21071  lidl1el  21136  drngnidl  21153  lidldvgen  21244  cnsubrg  21344  mulgrhm2  21388  znrrg  21475  ocvin  21583  ocvlsp  21585  mrccss  21603  topsn  22818  eltg4i  22847  unitg  22854  tgtop  22860  tgidm  22867  en2top  22872  basgen  22875  2basgen  22877  fctop  22891  cctop  22893  ppttop  22894  epttop  22896  ntrin  22948  isopn3  22953  opnnei  23007  neiuni  23009  maxlp  23034  clslp  23035  tgrest  23046  resttopon  23048  rest0  23056  restcls  23068  restntr  23069  ordtbas2  23078  ordtbas  23079  ordtrest2  23091  cmpcov2  23277  tgcmp  23288  cmpcld  23289  uncmp  23290  cmpfi  23295  dis2ndc  23347  restnlly  23369  dislly  23384  comppfsc  23419  kgentopon  23425  kgencmp  23432  kgenidm  23434  iskgen2  23435  kgencn3  23445  ptuni2  23463  ptbasfi  23468  xkouni  23486  txcls  23491  txdis  23519  txindis  23521  txcmplem2  23529  xkopt  23542  txconn  23576  qtopval2  23583  qtopuni  23589  qtoprest  23604  qtopomap  23605  qtopcmap  23606  kqsat  23618  kqcldsat  23620  hmeocls  23655  hmeontr  23656  hmphdis  23683  fgfil  23762  fgabs  23766  trfil1  23773  fgtr  23777  uzrest  23784  ufilmax  23794  ufileu  23806  filufint  23807  ufildom1  23813  rnelfm  23840  flimfil  23856  uffclsflim  23918  alexsublem  23931  alexsubALTlem3  23936  alexsubALT  23938  ptcmplem2  23940  ptcmplem3  23941  tgpconncompeqg  23999  haustsms2  24024  tgptsmscls  24037  ust0  24107  ustbas2  24113  iccntr  24710  pi1xfrcnv  24957  clsocv  25150  cfilfcls  25174  equivcmet  25217  hlhil  25343  evthicc2  25361  ovolshft  25412  volsup  25457  dyadmbllem  25500  mbfconstlem  25528  itg11  25592  limciun  25795  dvnres  25833  cpnord  25837  dvcmulf  25848  dvmptcmul  25868  dvcnvre  25924  plyco0  26097  taylthlem1  26281  taylthlem2  26282  taylthlem2OLD  26283  ulmdvlem3  26311  wilthlem2  26979  ppisval  27014  ppinprm  27062  chtnprm  27064  sltval2  27568  noextenddif  27580  scutun12  27722  madebdaylemlrcut  27810  cofcut1  27828  negsbday  27963  onsiso  28169  bdayon  28173  bdayn0p1  28258  upgrex  29019  uvtxnbgr  29327  cusgredg  29351  ubthlem1  30799  pjhth  31322  ococin  31337  chsupsn  31342  ssjo  31376  chabs1  31445  spansncvi  31581  mdslj1i  32248  mdslj2i  32249  atomli  32311  atcvatlem  32314  atcvat3i  32325  sumdmdlem  32347  difininv  32446  fnpreimac  32595  pmtrcnelor  33048  cycpmrn  33100  elrgspnlem4  33196  isdrng4  33245  fldgenid  33269  1fldgenq  33272  rspidlid  33346  0ringidl  33392  drngmxidl  33448  drngmxidlr  33449  resssra  33583  dimkerim  33623  fldextrspunlem1  33670  fldextrspunlem2  33672  algextdeglem4  33710  cmpcref  33840  zarcls1  33859  zarclssn  33863  zart0  33869  zarcmplem  33871  xpinpreima2  33897  ordtrest2NEW  33913  sigagenid  34141  imambfm  34253  reprinfz1  34613  bnj1136  34987  bnj1398  35024  bnj1408  35026  bnj1498  35051  fineqvacALT  35088  sconnpi1  35226  cvmliftlem15  35285  altopthsn  35949  opnbnd  36313  opnregcld  36318  cldregopn  36319  fnessref  36345  neibastop1  36347  topmeet  36352  topjoin  36353  fnemeet1  36354  fnejoin1  36356  bj-gabeqd  36925  bj-restpw  37080  bj-restb  37082  bj-restuni2  37086  dissneqlem  37328  pibt2  37405  lindsenlbs  37609  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  fdc  37739  sstotbnd2  37768  isbnd2  37777  totbndbnd  37783  prdstotbnd  37788  heibor1  37804  1idl  38020  igenval2  38060  idreseqidinxp  38297  disjdmqs  38796  lshpdisj  38980  lssats  39005  lsatcvat3  39045  lshpset2N  39112  lfl1dim  39114  lfl1dim2N  39115  lkrpssN  39156  paddass  39832  paddidm  39835  pmod1i  39842  pmapjat1  39847  pclbtwnN  39891  pclunN  39892  paddunN  39921  pclfinclN  39944  dihjust  41211  dihmeetlem1N  41284  dihglblem5apreN  41285  dihmeetlem13N  41313  dochocsp  41373  dochdmj1  41384  dochnoncon  41385  dihjatb  41410  dihjat1lem  41422  lcfl9a  41499  lclkrlem2s  41519  lclkrlem2v  41522  mapdrvallem3  41640  mapdunirnN  41644  mapdin  41656  mapdlsm  41658  baerlem3lem2  41704  baerlem5alem2  41705  baerlem5blem2  41706  hdmaplkr  41907  primrootsunit1  42085  sticksstones11  42144  aks6d1c6lem5  42165  unitscyglem4  42186  rntrclfvOAI  42679  ismrcd1  42686  ismrcd2  42687  isnacs3  42698  nacsfix  42700  rgspnid  43157  iocinico  43201  onsupmaxb  43228  onsssupeqcond  43269  oacl2g  43319  omabs2  43321  omcl2  43322  ofoaf  43344  onsucunifi  43359  naddwordnexlem4  43390  harval3  43527  mptrcllem  43602  clcnvlem  43612  dmtrcl  43616  rntrcl  43617  cbviuneq12df  43650  dfrcl2  43663  dftrcl3  43709  brtrclfv2  43716  dfrtrcl3  43722  scottrankd  44237  nzin  44307  iunincfi  45088  founiiun  45173  founiiun0  45184  inmap  45203  difmapsn  45206  funimaeq  45240  iuneqfzuz  45331  supminfrnmpt  45441  supminfxr2  45465  supminfxrrnmpt  45467  pimxrneun  45484  iooiinicc  45540  icomnfinre  45550  iooiinioc  45554  limsupresxr  45764  liminfresxr  45765  limsup10exlem  45770  liminfvalxr  45781  fourierdlem79  46183  rrxsnicc  46298  prsal  46316  issalgend  46336  sge0f1o  46380  caragenuni  46509  caragendifcl  46512  opnvonmbllem2  46631  iinhoiicc  46672  pimconstlt1  46700  pimltpnff  46701  pimiooltgt  46708  pimgtmnf2  46712  pimdecfgtioc  46713  pimincfltioc  46714  pimdecfgtioo  46715  pimincfltioo  46716  preimageiingt  46718  preimaleiinlt  46719  pimgtmnff  46720  sssmf  46736  smflimlem5  46773  smfmullem4  46792  smfpimbor1lem2  46797  smfsuplem1  46809  smfpimne2  46838  fsupdm  46840  finfdm  46844  sprsymrelf1  47497  lspeqlco  48428  iunlub  48809  iinglb  48810  iuneqconst2  48811  iineqconst2  48812  isclatd  48971  intubeu  48972  unilbeu  48973  setrecsres  49691