Theorem eqssd 3953

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

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

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 3920

This theorem is referenced by:  eqelssd  3957  uneqdifeq  4444  pweq  4565  unieq  4869  unissel  4889  intmin  4918  unissint  4922  int0el  4929  intidg  5400  dmcosseq  5919  dmcosseqOLD  5920  dmcosseqOLDOLD  5921  imadifssran  6100  sofld  6136  relfld  6223  preddowncl  6280  frpoind  6290  tz7.7  6333  f1imadifssran  6568  knatar  7294  sorpssuni  7668  sorpssint  7669  onint  7726  fo2ndf  8054  suppimacnv  8107  tposeq  8161  frrlem14  8232  onfununi  8264  tfrlem15  8314  oaass  8479  odi  8497  omass  8498  oelim2  8513  oeeui  8520  nnawordex  8555  oaabslem  8565  oaabs2  8567  omabslem  8568  omabs  8569  cofon1  8590  uniinqs  8724  sucdom2  9117  onomeneq  9128  fineqv  9156  dffi2  9313  fiuni  9318  dffi3  9321  hartogslem1  9434  ixpiunwdom  9482  cantnfp1lem3  9576  oemapvali  9580  cantnf  9589  dfttrcl2  9620  frind  9646  r1val1  9682  rankval3b  9722  rankunb  9746  rankuni2b  9749  rankr1id  9758  rankc2  9767  rankxplim  9775  tcrank  9780  carden2b  9863  harval2  9893  en2other2  9903  infpwfien  9956  coflim  10155  cfcof  10168  cfidm  10169  isf32lem2  10248  fin1a2lem11  10304  fin1a2lem13  10306  ttukeylem7  10409  fpwwe2  10537  winafp  10591  wuncidm  10640  wuncval2  10641  tskuni  10677  grur1  10714  distrpr  10922  ltexpri  10937  reclem4pr  10944  fzopth  13464  fzosplit  13595  fzouzsplit  13597  fzoopth  13665  ccatrn  14496  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  18556  gsumvallem2  18708  gsumwspan  18720  trivsubgd  19032  trivsubgsnd  19033  trivnsgd  19051  cycsubg  19087  kerf1ghm  19126  conjnmz  19131  pmtrprfv  19332  symggen  19349  odf1o2  19452  gex1  19470  sylow2alem1  19496  smndlsmidm  19535  lsmss1  19544  lsmss2  19546  lsmmod  19554  lsmdisj  19560  lsmdisj2  19561  cntzcmn  19719  prmcyg  19773  dmdprdd  19880  dprdspan  19908  dprdres  19909  dprdz  19911  subgdmdprd  19915  subgdprd  19916  dprddisj2  19920  dprd2dlem1  19922  dprd2da  19923  dmdprdsplit2lem  19926  dprdsplit  19929  ablfacrp  19947  pgpfac1lem3  19958  issubdrg  20665  lspun  20890  lspsn  20905  lspsnneg  20909  lsp0  20912  lsslsp  20918  lsslspOLD  20919  lmhmlsp  20953  lspextmo  20960  lsmsp  20990  lspprabs  20999  lspsnvs  21021  lspdisj  21032  lsmcv  21048  lspsnat  21052  lsppratlem6  21059  lspprat  21060  lbsextlem4  21068  lidl1el  21133  drngnidl  21150  lidldvgen  21241  cnsubrg  21334  mulgrhm2  21385  znrrg  21472  ocvin  21581  ocvlsp  21583  mrccss  21601  topsn  22816  eltg4i  22845  unitg  22852  tgtop  22858  tgidm  22865  en2top  22870  basgen  22873  2basgen  22875  fctop  22889  cctop  22891  ppttop  22892  epttop  22894  ntrin  22946  isopn3  22951  opnnei  23005  neiuni  23007  maxlp  23032  clslp  23033  tgrest  23044  resttopon  23046  rest0  23054  restcls  23066  restntr  23067  ordtbas2  23076  ordtbas  23077  ordtrest2  23089  cmpcov2  23275  tgcmp  23286  cmpcld  23287  uncmp  23288  cmpfi  23293  dis2ndc  23345  restnlly  23367  dislly  23382  comppfsc  23417  kgentopon  23423  kgencmp  23430  kgenidm  23432  iskgen2  23433  kgencn3  23443  ptuni2  23461  ptbasfi  23466  xkouni  23484  txcls  23489  txdis  23517  txindis  23519  txcmplem2  23527  xkopt  23540  txconn  23574  qtopval2  23581  qtopuni  23587  qtoprest  23602  qtopomap  23603  qtopcmap  23604  kqsat  23616  kqcldsat  23618  hmeocls  23653  hmeontr  23654  hmphdis  23681  fgfil  23760  fgabs  23764  trfil1  23771  fgtr  23775  uzrest  23782  ufilmax  23792  ufileu  23804  filufint  23805  ufildom1  23811  rnelfm  23838  flimfil  23854  uffclsflim  23916  alexsublem  23929  alexsubALTlem3  23934  alexsubALT  23936  ptcmplem2  23938  ptcmplem3  23939  tgpconncompeqg  23997  haustsms2  24022  tgptsmscls  24035  ust0  24105  ustbas2  24111  iccntr  24708  pi1xfrcnv  24955  clsocv  25148  cfilfcls  25172  equivcmet  25215  hlhil  25341  evthicc2  25359  ovolshft  25410  volsup  25455  dyadmbllem  25498  mbfconstlem  25526  itg11  25590  limciun  25793  dvnres  25831  cpnord  25835  dvcmulf  25846  dvmptcmul  25866  dvcnvre  25922  plyco0  26095  taylthlem1  26279  taylthlem2  26280  taylthlem2OLD  26281  ulmdvlem3  26309  wilthlem2  26977  ppisval  27012  ppinprm  27060  chtnprm  27062  sltval2  27566  noextenddif  27578  scutun12  27721  madebdaylemlrcut  27813  bdayiun  27829  cofcut1  27833  negsbday  27968  onsiso  28174  bdayon  28178  bdayn0p1  28263  upgrex  29037  uvtxnbgr  29345  cusgredg  29369  ubthlem1  30814  pjhth  31337  ococin  31352  chsupsn  31357  ssjo  31391  chabs1  31460  spansncvi  31596  mdslj1i  32263  mdslj2i  32264  atomli  32326  atcvatlem  32329  atcvat3i  32340  sumdmdlem  32362  difininv  32461  fnpreimac  32614  pmtrcnelor  33033  cycpmrn  33085  elrgspnlem4  33185  isdrng4  33234  fldgenid  33258  1fldgenq  33261  rspidlid  33312  0ringidl  33358  drngmxidl  33414  drngmxidlr  33415  resssra  33553  dimkerim  33594  fldextrspunlem1  33642  fldextrspunlem2  33644  algextdeglem4  33687  cmpcref  33817  zarcls1  33836  zarclssn  33840  zart0  33846  zarcmplem  33848  xpinpreima2  33874  ordtrest2NEW  33890  sigagenid  34118  imambfm  34230  reprinfz1  34590  bnj1136  34964  bnj1398  35001  bnj1408  35003  bnj1498  35028  fineqvacALT  35073  sconnpi1  35216  cvmliftlem15  35275  altopthsn  35939  opnbnd  36303  opnregcld  36308  cldregopn  36309  fnessref  36335  neibastop1  36337  topmeet  36342  topjoin  36343  fnemeet1  36344  fnejoin1  36346  bj-gabeqd  36915  bj-restpw  37070  bj-restb  37072  bj-restuni2  37076  dissneqlem  37318  pibt2  37395  lindsenlbs  37599  poimirlem13  37617  poimirlem14  37618  poimirlem15  37619  fdc  37729  sstotbnd2  37758  isbnd2  37767  totbndbnd  37773  prdstotbnd  37778  heibor1  37794  1idl  38010  igenval2  38050  idreseqidinxp  38287  disjdmqs  38786  lshpdisj  38970  lssats  38995  lsatcvat3  39035  lshpset2N  39102  lfl1dim  39104  lfl1dim2N  39105  lkrpssN  39146  paddass  39821  paddidm  39824  pmod1i  39831  pmapjat1  39836  pclbtwnN  39880  pclunN  39881  paddunN  39910  pclfinclN  39933  dihjust  41200  dihmeetlem1N  41273  dihglblem5apreN  41274  dihmeetlem13N  41302  dochocsp  41362  dochdmj1  41373  dochnoncon  41374  dihjatb  41399  dihjat1lem  41411  lcfl9a  41488  lclkrlem2s  41508  lclkrlem2v  41511  mapdrvallem3  41629  mapdunirnN  41633  mapdin  41645  mapdlsm  41647  baerlem3lem2  41693  baerlem5alem2  41694  baerlem5blem2  41695  hdmaplkr  41896  primrootsunit1  42074  sticksstones11  42133  aks6d1c6lem5  42154  unitscyglem4  42175  rntrclfvOAI  42668  ismrcd1  42675  ismrcd2  42676  isnacs3  42687  nacsfix  42689  rgspnid  43145  iocinico  43189  onsupmaxb  43216  onsssupeqcond  43257  oacl2g  43307  omabs2  43309  omcl2  43310  ofoaf  43332  onsucunifi  43347  naddwordnexlem4  43378  harval3  43515  mptrcllem  43590  clcnvlem  43600  dmtrcl  43604  rntrcl  43605  cbviuneq12df  43638  dfrcl2  43651  dftrcl3  43697  brtrclfv2  43704  dfrtrcl3  43710  scottrankd  44225  nzin  44295  iunincfi  45076  founiiun  45161  founiiun0  45172  inmap  45191  difmapsn  45194  funimaeq  45228  iuneqfzuz  45319  supminfrnmpt  45428  supminfxr2  45452  supminfxrrnmpt  45454  pimxrneun  45471  iooiinicc  45527  icomnfinre  45537  iooiinioc  45541  limsupresxr  45751  liminfresxr  45752  limsup10exlem  45757  liminfvalxr  45768  fourierdlem79  46170  rrxsnicc  46285  prsal  46303  issalgend  46323  sge0f1o  46367  caragenuni  46496  caragendifcl  46499  opnvonmbllem2  46618  iinhoiicc  46659  pimconstlt1  46687  pimltpnff  46688  pimiooltgt  46695  pimgtmnf2  46699  pimdecfgtioc  46700  pimincfltioc  46701  pimdecfgtioo  46702  pimincfltioo  46703  preimageiingt  46705  preimaleiinlt  46706  pimgtmnff  46707  sssmf  46723  smflimlem5  46760  smfmullem4  46779  smfpimbor1lem2  46784  smfsuplem1  46796  smfpimne2  46825  fsupdm  46827  finfdm  46831  sprsymrelf1  47484  lspeqlco  48428  iunlub  48809  iinglb  48810  iuneqconst2  48811  iineqconst2  48812  isclatd  48971  intubeu  48972  unilbeu  48973  setrecsres  49691