Theorem eqssd 3983

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ss 3950

This theorem is referenced by:  eqelssd  3987  uneqdifeq  4475  pweq  4596  unieq  4900  unissel  4920  intmin  4950  unissint  4954  int0el  4961  intidg  5444  dmcosseq  5969  dmcosseqOLD  5970  imadifssran  6153  sofld  6189  relfld  6277  preddowncl  6334  frpoind  6344  wfiOLD  6353  tz7.7  6391  f1imadifssran  6633  knatar  7360  sorpssuni  7735  sorpssint  7736  onint  7793  fo2ndf  8129  suppimacnv  8182  tposeq  8236  frrlem14  8307  onfununi  8364  tfrlem15  8415  oaass  8582  odi  8600  omass  8601  oelim2  8616  oeeui  8623  nnawordex  8658  oaabslem  8668  oaabs2  8670  omabslem  8671  omabs  8672  cofon1  8693  uniinqs  8820  sucdom2OLD  9105  sucdom2  9226  onomeneq  9248  fineqv  9282  dffi2  9446  fiuni  9451  dffi3  9454  hartogslem1  9565  ixpiunwdom  9613  cantnfp1lem3  9703  oemapvali  9707  cantnf  9716  dfttrcl2  9747  frind  9773  r1val1  9809  rankval3b  9849  rankunb  9873  rankuni2b  9876  rankr1id  9885  rankc2  9894  rankxplim  9902  tcrank  9907  carden2b  9990  harval2  10020  en2other2  10032  infpwfien  10085  coflim  10284  cfcof  10297  cfidm  10298  isf32lem2  10377  fin1a2lem11  10433  fin1a2lem13  10435  ttukeylem7  10538  fpwwe2  10666  winafp  10720  wuncidm  10769  wuncval2  10770  tskuni  10806  grur1  10843  distrpr  11051  ltexpri  11066  reclem4pr  11073  fzopth  13584  fzosplit  13715  fzouzsplit  13717  fzoopth  13784  ccatrn  14610  cotrtrclfv  15034  dmtrclfv  15040  dfrtrcl2  15084  structcnvcnv  17173  imasaddfnlem  17549  imasvscafn  17558  mrcuni  17640  mressmrcd  17646  submrc  17647  ssceq  17846  rescabs  17853  rescabsOLD  17854  setcepi  18109  clatl  18527  ipopos  18555  psdmrn  18592  dirdm  18619  gsumress  18669  gsumvallem2  18821  gsumwspan  18833  trivsubgd  19145  trivsubgsnd  19146  trivnsgd  19164  cycsubg  19200  kerf1ghm  19239  conjnmz  19244  pmtrprfv  19444  symggen  19461  odf1o2  19564  gex1  19582  sylow2alem1  19608  smndlsmidm  19647  lsmss1  19656  lsmss2  19658  lsmmod  19666  lsmdisj  19672  lsmdisj2  19673  cntzcmn  19831  prmcyg  19885  dmdprdd  19992  dprdspan  20020  dprdres  20021  dprdz  20023  subgdmdprd  20027  subgdprd  20028  dprddisj2  20032  dprd2dlem1  20034  dprd2da  20035  dmdprdsplit2lem  20038  dprdsplit  20041  ablfacrp  20059  pgpfac1lem3  20070  issubdrg  20754  lspun  20958  lspsn  20973  lspsnneg  20977  lsp0  20980  lsslsp  20986  lsslspOLD  20987  lmhmlsp  21021  lspextmo  21028  lsmsp  21058  lspprabs  21067  lspsnvs  21089  lspdisj  21100  lsmcv  21116  lspsnat  21120  lsppratlem6  21127  lspprat  21128  lbsextlem4  21136  lidl1el  21203  drngnidl  21220  lidldvgen  21311  cnsubrg  21412  mulgrhm2  21456  znrrg  21551  ocvin  21659  ocvlsp  21661  mrccss  21679  topsn  22904  eltg4i  22933  unitg  22940  tgtop  22946  tgidm  22953  en2top  22958  basgen  22961  2basgen  22963  fctop  22977  cctop  22979  ppttop  22980  epttop  22982  ntrin  23034  isopn3  23039  opnnei  23093  neiuni  23095  maxlp  23120  clslp  23121  tgrest  23132  resttopon  23134  rest0  23142  restcls  23154  restntr  23155  ordtbas2  23164  ordtbas  23165  ordtrest2  23177  cmpcov2  23363  tgcmp  23374  cmpcld  23375  uncmp  23376  cmpfi  23381  dis2ndc  23433  restnlly  23455  dislly  23470  comppfsc  23505  kgentopon  23511  kgencmp  23518  kgenidm  23520  iskgen2  23521  kgencn3  23531  ptuni2  23549  ptbasfi  23554  xkouni  23572  txcls  23577  txdis  23605  txindis  23607  txcmplem2  23615  xkopt  23628  txconn  23662  qtopval2  23669  qtopuni  23675  qtoprest  23690  qtopomap  23691  qtopcmap  23692  kqsat  23704  kqcldsat  23706  hmeocls  23741  hmeontr  23742  hmphdis  23769  fgfil  23848  fgabs  23852  trfil1  23859  fgtr  23863  uzrest  23870  ufilmax  23880  ufileu  23892  filufint  23893  ufildom1  23899  rnelfm  23926  flimfil  23942  uffclsflim  24004  alexsublem  24017  alexsubALTlem3  24022  alexsubALT  24024  ptcmplem2  24026  ptcmplem3  24027  tgpconncompeqg  24085  haustsms2  24110  tgptsmscls  24123  ust0  24193  ustbas2  24199  iccntr  24798  pi1xfrcnv  25045  clsocv  25239  cfilfcls  25263  equivcmet  25306  hlhil  25432  evthicc2  25450  ovolshft  25501  volsup  25546  dyadmbllem  25589  mbfconstlem  25617  itg11  25681  limciun  25884  dvnres  25922  cpnord  25926  dvcmulf  25937  dvmptcmul  25957  dvcnvre  26013  plyco0  26186  taylthlem1  26370  taylthlem2  26371  taylthlem2OLD  26372  ulmdvlem3  26400  wilthlem2  27067  ppisval  27102  ppinprm  27150  chtnprm  27152  sltval2  27656  noextenddif  27668  scutun12  27810  madebdaylemlrcut  27892  cofcut1  27909  negsbday  28044  upgrex  29056  uvtxnbgr  29364  cusgredg  29388  ubthlem1  30836  pjhth  31359  ococin  31374  chsupsn  31379  ssjo  31413  chabs1  31482  spansncvi  31618  mdslj1i  32285  mdslj2i  32286  atomli  32348  atcvatlem  32351  atcvat3i  32362  sumdmdlem  32384  difininv  32483  fnpreimac  32628  pmtrcnelor  33057  cycpmrn  33109  elrgspnlem4  33195  isdrng4  33244  fldgenid  33267  1fldgenq  33270  rspidlid  33344  0ringidl  33390  drngmxidl  33446  drngmxidlr  33447  resssra  33579  dimkerim  33619  fldextrspunlem1  33666  fldextrspunlem2  33668  algextdeglem4  33702  cmpcref  33790  zarcls1  33809  zarclssn  33813  zart0  33819  zarcmplem  33821  xpinpreima2  33847  ordtrest2NEW  33863  sigagenid  34093  imambfm  34205  reprinfz1  34578  bnj1136  34952  bnj1398  34989  bnj1408  34991  bnj1498  35016  fineqvacALT  35053  sconnpi1  35185  cvmliftlem15  35244  altopthsn  35903  opnbnd  36267  opnregcld  36272  cldregopn  36273  fnessref  36299  neibastop1  36301  topmeet  36306  topjoin  36307  fnemeet1  36308  fnejoin1  36310  bj-gabeqd  36879  bj-restpw  37034  bj-restb  37036  bj-restuni2  37040  dissneqlem  37282  pibt2  37359  lindsenlbs  37563  poimirlem13  37581  poimirlem14  37582  poimirlem15  37583  fdc  37693  sstotbnd2  37722  isbnd2  37731  totbndbnd  37737  prdstotbnd  37742  heibor1  37758  1idl  37974  igenval2  38014  idreseqidinxp  38251  disjdmqs  38746  lshpdisj  38929  lssats  38954  lsatcvat3  38994  lshpset2N  39061  lfl1dim  39063  lfl1dim2N  39064  lkrpssN  39105  paddass  39781  paddidm  39784  pmod1i  39791  pmapjat1  39796  pclbtwnN  39840  pclunN  39841  paddunN  39870  pclfinclN  39893  dihjust  41160  dihmeetlem1N  41233  dihglblem5apreN  41234  dihmeetlem13N  41262  dochocsp  41322  dochdmj1  41333  dochnoncon  41334  dihjatb  41359  dihjat1lem  41371  lcfl9a  41448  lclkrlem2s  41468  lclkrlem2v  41471  mapdrvallem3  41589  mapdunirnN  41593  mapdin  41605  mapdlsm  41607  baerlem3lem2  41653  baerlem5alem2  41654  baerlem5blem2  41655  hdmaplkr  41856  primrootsunit1  42039  sticksstones11  42098  aks6d1c6lem5  42119  unitscyglem4  42140  rntrclfvOAI  42647  ismrcd1  42654  ismrcd2  42655  isnacs3  42666  nacsfix  42668  rgspnid  43125  iocinico  43169  onsupmaxb  43196  onsssupeqcond  43238  oacl2g  43288  omabs2  43290  omcl2  43291  ofoaf  43313  onsucunifi  43328  naddwordnexlem4  43359  harval3  43496  mptrcllem  43571  clcnvlem  43581  dmtrcl  43585  rntrcl  43586  cbviuneq12df  43619  dfrcl2  43632  dftrcl3  43678  brtrclfv2  43685  dfrtrcl3  43691  scottrankd  44212  nzin  44282  iunincfi  45044  founiiun  45129  founiiun0  45140  inmap  45159  difmapsn  45162  funimaeq  45198  iuneqfzuz  45291  supminfrnmpt  45401  supminfxr2  45425  supminfxrrnmpt  45427  pimxrneun  45444  iooiinicc  45500  icomnfinre  45510  iooiinioc  45514  limsupresxr  45726  liminfresxr  45727  limsup10exlem  45732  liminfvalxr  45743  fourierdlem79  46145  rrxsnicc  46260  prsal  46278  issalgend  46298  sge0f1o  46342  caragenuni  46471  caragendifcl  46474  opnvonmbllem2  46593  iinhoiicc  46634  pimconstlt1  46662  pimltpnff  46663  pimiooltgt  46670  pimgtmnf2  46674  pimdecfgtioc  46675  pimincfltioc  46676  pimdecfgtioo  46677  pimincfltioo  46678  preimageiingt  46680  preimaleiinlt  46681  pimgtmnff  46682  sssmf  46698  smflimlem5  46735  smfmullem4  46754  smfpimbor1lem2  46759  smfsuplem1  46771  smfpimne2  46800  fsupdm  46802  finfdm  46806  sprsymrelf1  47429  lspeqlco  48302  isclatd  48828  intubeu  48829  unilbeu  48830  setrecsres  49217