Theorem eqssd 3932

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

Syntax hints:   → wi 4   = wceq 1547   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  eqelssd  3936  uneqdifeq  4420  pweq  4543  unieq  4849  unissel  4870  intmin  4898  unissint  4902  int0el  4909  intidg  5396  dmcosseq  5920  dmcosseqOLD  5921  dmcosseqOLDOLD  5922  imadifssran  6102  sofld  6138  relfld  6226  preddowncl  6283  frpoind  6293  tz7.7  6336  f1imadifssran  6571  knatar  7301  sorpssuni  7675  sorpssint  7676  onint  7733  fo2ndf  8060  suppimacnv  8114  tposeq  8168  frrlem14  8239  onfununi  8271  tfrlem15  8321  oaass  8486  odi  8504  omass  8505  oelim2  8521  oeeui  8528  nnawordex  8563  oaabslem  8573  oaabs2  8575  omabslem  8576  omabs  8577  cofon1  8598  uniinqs  8734  sucdom2  9127  onomeneq  9138  fineqv  9167  dffi2  9326  fiuni  9331  dffi3  9334  hartogslem1  9447  ixpiunwdom  9495  cantnfp1lem3  9592  oemapvali  9596  cantnf  9605  dfttrcl2  9636  frind  9665  r1val1  9701  rankval3b  9741  rankunb  9765  rankuni2b  9768  rankr1id  9777  rankc2  9786  rankxplim  9794  tcrank  9799  carden2b  9882  harval2  9912  en2other2  9922  infpwfien  9975  coflim  10174  cfcof  10187  cfidm  10188  isf32lem2  10267  fin1a2lem11  10323  fin1a2lem13  10325  ttukeylem7  10428  fpwwe2  10557  winafp  10611  wuncidm  10660  wuncval2  10661  tskuni  10697  grur1  10734  distrpr  10942  ltexpri  10957  reclem4pr  10964  fzopth  13506  fzosplit  13638  fzouzsplit  13640  fzoopth  13708  ccatrn  14543  cotrtrclfv  14965  dmtrclfv  14971  dfrtrcl2  15015  structcnvcnv  17114  imasaddfnlem  17483  imasvscafn  17492  mrcuni  17578  mressmrcd  17584  submrc  17585  ssceq  17784  rescabs  17791  setcepi  18046  clatl  18465  ipopos  18493  psdmrn  18530  dirdm  18557  gsumress  18641  gsumvallem2  18793  gsumwspan  18805  trivsubgd  19119  trivsubgsnd  19120  trivnsgd  19138  cycsubg  19174  kerf1ghm  19213  conjnmz  19218  pmtrprfv  19419  symggen  19436  odf1o2  19539  gex1  19557  sylow2alem1  19583  smndlsmidm  19622  lsmss1  19631  lsmss2  19633  lsmmod  19641  lsmdisj  19647  lsmdisj2  19648  cntzcmn  19806  prmcyg  19860  dmdprdd  19967  dprdspan  19995  dprdres  19996  dprdz  19998  subgdmdprd  20002  subgdprd  20003  dprddisj2  20007  dprd2dlem1  20009  dprd2da  20010  dmdprdsplit2lem  20013  dprdsplit  20016  ablfacrp  20034  pgpfac1lem3  20045  issubdrg  20752  lspun  20977  lspsn  20992  lspsnneg  20996  lsp0  20999  lsslsp  21005  lmhmlsp  21039  lspextmo  21046  lsmsp  21076  lspprabs  21085  lspsnvs  21107  lspdisj  21118  lsmcv  21134  lspsnat  21138  lsppratlem6  21145  lspprat  21146  lbsextlem4  21154  lidl1el  21219  drngnidl  21236  lidldvgen  21327  cnsubrg  21402  mulgrhm2  21453  znrrg  21540  ocvin  21649  ocvlsp  21651  mrccss  21669  topsn  22914  eltg4i  22943  unitg  22950  tgtop  22956  tgidm  22963  en2top  22968  basgen  22971  2basgen  22973  fctop  22987  cctop  22989  ppttop  22990  epttop  22992  ntrin  23044  isopn3  23049  opnnei  23103  neiuni  23105  maxlp  23130  clslp  23131  tgrest  23142  resttopon  23144  rest0  23152  restcls  23164  restntr  23165  ordtbas2  23174  ordtbas  23175  ordtrest2  23187  cmpcov2  23373  tgcmp  23384  cmpcld  23385  uncmp  23386  cmpfi  23391  dis2ndc  23443  restnlly  23465  dislly  23480  comppfsc  23515  kgentopon  23521  kgencmp  23528  kgenidm  23530  iskgen2  23531  kgencn3  23541  ptuni2  23559  ptbasfi  23564  xkouni  23582  txcls  23587  txdis  23615  txindis  23617  txcmplem2  23625  xkopt  23638  txconn  23672  qtopval2  23679  qtopuni  23685  qtoprest  23700  qtopomap  23701  qtopcmap  23702  kqsat  23714  kqcldsat  23716  hmeocls  23751  hmeontr  23752  hmphdis  23779  fgfil  23858  fgabs  23862  trfil1  23869  fgtr  23873  uzrest  23880  ufilmax  23890  ufileu  23902  filufint  23903  ufildom1  23909  rnelfm  23936  flimfil  23952  uffclsflim  24014  alexsublem  24027  alexsubALTlem3  24032  alexsubALT  24034  ptcmplem2  24036  ptcmplem3  24037  tgpconncompeqg  24095  haustsms2  24120  tgptsmscls  24133  ust0  24203  ustbas2  24208  iccntr  24805  pi1xfrcnv  25042  clsocv  25235  cfilfcls  25259  equivcmet  25302  hlhil  25428  evthicc2  25445  ovolshft  25496  volsup  25541  dyadmbllem  25584  mbfconstlem  25612  itg11  25676  limciun  25879  dvnres  25916  cpnord  25920  dvcmulf  25930  dvmptcmul  25949  dvcnvre  26004  plyco0  26175  taylthlem1  26356  taylthlem2  26357  ulmdvlem3  26385  wilthlem2  27050  ppisval  27085  ppinprm  27133  chtnprm  27135  ltsval2  27638  noextenddif  27650  cutsun12  27800  madebdaylemlrcut  27909  bdayiun  27925  cofcut1  27930  negbday  28067  oniso  28281  bdayons  28286  addonbday  28289  bdayn0p1  28379  upgrex  29179  uvtxnbgr  29487  cusgredg  29511  ubthlem1  30959  pjhth  31482  ococin  31497  chsupsn  31502  ssjo  31536  chabs1  31605  spansncvi  31741  mdslj1i  32408  mdslj2i  32409  atomli  32471  atcvatlem  32474  atcvat3i  32485  sumdmdlem  32507  difininv  32605  fnpreimac  32762  pmtrcnelor  33172  cycpmrn  33224  elrgspnlem4  33326  isdrng4  33379  fldgenid  33403  1fldgenq  33406  rspidlid  33458  0ringidl  33504  drngmxidl  33560  drngmxidlr  33561  esplyfvaln  33758  resssra  33771  dimkerim  33811  fldextrspunlem1  33859  fldextrspunlem2  33861  algextdeglem4  33904  cmpcref  34034  zarcls1  34053  zarclssn  34057  zart0  34063  zarcmplem  34065  xpinpreima2  34091  ordtrest2NEW  34107  sigagenid  34335  imambfm  34446  reprinfz1  34806  bnj1136  35179  bnj1398  35216  bnj1408  35218  bnj1498  35243  rankval4b  35281  r1omhfb  35293  fineqvacALT  35298  r1omhfbregs  35318  sconnpi1  35467  cvmliftlem15  35526  altopthsn  36189  opnbnd  36553  opnregcld  36558  cldregopn  36559  fnessref  36585  neibastop1  36587  topmeet  36592  topjoin  36593  fnemeet1  36594  fnejoin1  36596  ttctrid  36730  dfttc2g  36734  dfttc3gw  36751  bj-gabeqd  37290  bj-restpw  37450  bj-restb  37452  bj-restuni2  37456  dissneqlem  37702  pibt2  37779  lindsenlbs  37982  poimirlem13  38000  poimirlem14  38001  poimirlem15  38002  fdc  38112  sstotbnd2  38141  isbnd2  38150  totbndbnd  38156  prdstotbnd  38161  heibor1  38177  1idl  38393  igenval2  38433  idreseqidinxp  38682  disjdmqs  39274  lshpdisj  39479  lssats  39504  lsatcvat3  39544  lshpset2N  39611  lfl1dim  39613  lfl1dim2N  39614  lkrpssN  39655  paddass  40330  paddidm  40333  pmod1i  40340  pmapjat1  40345  pclbtwnN  40389  pclunN  40390  paddunN  40419  pclfinclN  40442  dihjust  41709  dihmeetlem1N  41782  dihglblem5apreN  41783  dihmeetlem13N  41811  dochocsp  41871  dochdmj1  41882  dochnoncon  41883  dihjatb  41908  dihjat1lem  41920  lcfl9a  41997  lclkrlem2s  42017  lclkrlem2v  42020  mapdrvallem3  42138  mapdunirnN  42142  mapdin  42154  mapdlsm  42156  baerlem3lem2  42202  baerlem5alem2  42203  baerlem5blem2  42204  hdmaplkr  42405  primrootsunit1  42582  sticksstones11  42641  aks6d1c6lem5  42662  unitscyglem4  42683  rntrclfvOAI  43140  ismrcd1  43147  ismrcd2  43148  isnacs3  43159  nacsfix  43161  rgspnid  43613  iocinico  43657  onsupmaxb  43684  onsssupeqcond  43725  oacl2g  43775  omabs2  43777  omcl2  43778  ofoaf  43800  onsucunifi  43815  naddwordnexlem4  43846  harval3  43982  mptrcllem  44057  clcnvlem  44067  dmtrcl  44071  rntrcl  44072  cbviuneq12df  44105  dfrcl2  44118  dftrcl3  44164  brtrclfv2  44171  dfrtrcl3  44177  scottrankd  44692  nzin  44762  iunincfi  45541  founiiun  45626  founiiun0  45637  inmap  45654  difmapsn  45657  funimaeq  45690  iuneqfzuz  45780  supminfrnmpt  45888  supminfxr2  45912  supminfxrrnmpt  45914  pimxrneun  45931  iooiinicc  45987  icomnfinre  45997  iooiinioc  46001  limsupresxr  46209  liminfresxr  46210  limsup10exlem  46215  liminfvalxr  46226  fourierdlem79  46628  rrxsnicc  46743  prsal  46761  issalgend  46781  sge0f1o  46825  caragenuni  46954  caragendifcl  46957  opnvonmbllem2  47076  iinhoiicc  47117  pimconstlt1  47145  pimltpnff  47146  pimiooltgt  47153  pimgtmnf2  47157  pimdecfgtioc  47158  pimincfltioc  47159  pimdecfgtioo  47160  pimincfltioo  47161  preimageiingt  47163  preimaleiinlt  47164  pimgtmnff  47165  sssmf  47181  smflimlem5  47218  smfmullem4  47237  smfpimbor1lem2  47242  smfsuplem1  47254  smfpimne2  47283  fsupdm  47285  finfdm  47289  sprsymrelf1  47971  lspeqlco  48930  iunlub  49311  iinglb  49312  iuneqconst2  49313  iineqconst2  49314  isclatd  49473  intubeu  49474  unilbeu  49475  setrecsres  50192