Theorem eqssd 4000

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  eqelssd  4004  uneqdifeq  4493  pweq  4617  unieq  4920  unissel  4943  intmin  4973  unissint  4977  int0el  4984  intidg  5458  dmcosseq  5973  sofld  6187  relfld  6275  preddowncl  6334  frpoind  6344  wfiOLD  6353  tz7.7  6391  fimacnvOLD  7073  knatar  7354  sorpssuni  7722  sorpssint  7723  onint  7778  fo2ndf  8107  suppimacnv  8159  tposeq  8213  frrlem14  8284  onfununi  8341  tfrlem15  8392  oaass  8561  odi  8579  omass  8580  oelim2  8595  oeeui  8602  nnawordex  8637  oaabslem  8646  oaabs2  8648  omabslem  8649  omabs  8650  cofon1  8671  uniinqs  8791  sucdom2OLD  9082  sucdom2  9206  onomeneq  9228  fineqv  9263  dffi2  9418  fiuni  9423  dffi3  9426  hartogslem1  9537  ixpiunwdom  9585  cantnfp1lem3  9675  oemapvali  9679  cantnf  9688  dfttrcl2  9719  frind  9745  r1val1  9781  rankval3b  9821  rankunb  9845  rankuni2b  9848  rankr1id  9857  rankc2  9866  rankxplim  9874  tcrank  9879  carden2b  9962  harval2  9992  en2other2  10004  infpwfien  10057  coflim  10256  cfcof  10269  cfidm  10270  isf32lem2  10349  fin1a2lem11  10405  fin1a2lem13  10407  ttukeylem7  10510  fpwwe2  10638  winafp  10692  wuncidm  10741  wuncval2  10742  tskuni  10778  grur1  10815  distrpr  11023  ltexpri  11038  reclem4pr  11045  fzopth  13538  fzosplit  13665  fzouzsplit  13667  ccatrn  14539  cotrtrclfv  14959  dmtrclfv  14965  dfrtrcl2  15009  structcnvcnv  17086  imasaddfnlem  17474  imasvscafn  17483  mrcuni  17565  mressmrcd  17571  submrc  17572  ssceq  17773  rescabs  17782  rescabsOLD  17783  setcepi  18038  clatl  18461  ipopos  18489  psdmrn  18526  dirdm  18553  gsumress  18601  gsumvallem2  18715  gsumwspan  18727  trivsubgd  19033  trivsubgsnd  19034  trivnsgd  19052  cycsubg  19085  conjnmz  19126  pmtrprfv  19321  symggen  19338  odf1o2  19441  gex1  19459  sylow2alem1  19485  smndlsmidm  19524  lsmss1  19533  lsmss2  19535  lsmmod  19543  lsmdisj  19549  lsmdisj2  19550  cntzcmn  19708  prmcyg  19762  dmdprdd  19869  dprdspan  19897  dprdres  19898  dprdz  19900  subgdmdprd  19904  subgdprd  19905  dprddisj2  19909  dprd2dlem1  19911  dprd2da  19912  dmdprdsplit2lem  19915  dprdsplit  19918  ablfacrp  19936  pgpfac1lem3  19947  kerf1ghm  20282  issubdrg  20401  lspun  20598  lspsn  20613  lspsnneg  20617  lsp0  20620  lsslsp  20626  lmhmlsp  20660  lspextmo  20667  lsmsp  20697  lspprabs  20706  lspsnvs  20727  lspdisj  20738  lsmcv  20754  lspsnat  20758  lsppratlem6  20765  lspprat  20766  lbsextlem4  20774  lidl1el  20841  drngnidl  20854  lidldvgen  20893  cnsubrg  21005  mulgrhm2  21048  znrrg  21121  ocvin  21227  ocvlsp  21229  mrccss  21247  topsn  22433  eltg4i  22463  unitg  22470  tgtop  22476  tgidm  22483  en2top  22488  basgen  22491  2basgen  22493  fctop  22507  cctop  22509  ppttop  22510  epttop  22512  ntrin  22565  isopn3  22570  opnnei  22624  neiuni  22626  maxlp  22651  clslp  22652  tgrest  22663  resttopon  22665  rest0  22673  restcls  22685  restntr  22686  ordtbas2  22695  ordtbas  22696  ordtrest2  22708  cmpcov2  22894  tgcmp  22905  cmpcld  22906  uncmp  22907  cmpfi  22912  dis2ndc  22964  restnlly  22986  dislly  23001  comppfsc  23036  kgentopon  23042  kgencmp  23049  kgenidm  23051  iskgen2  23052  kgencn3  23062  ptuni2  23080  ptbasfi  23085  xkouni  23103  txcls  23108  txdis  23136  txindis  23138  txcmplem2  23146  xkopt  23159  txconn  23193  qtopval2  23200  qtopuni  23206  qtoprest  23221  qtopomap  23222  qtopcmap  23223  kqsat  23235  kqcldsat  23237  hmeocls  23272  hmeontr  23273  hmphdis  23300  fgfil  23379  fgabs  23383  trfil1  23390  fgtr  23394  uzrest  23401  ufilmax  23411  ufileu  23423  filufint  23424  ufildom1  23430  rnelfm  23457  flimfil  23473  uffclsflim  23535  alexsublem  23548  alexsubALTlem3  23553  alexsubALT  23555  ptcmplem2  23557  ptcmplem3  23558  tgpconncompeqg  23616  haustsms2  23641  tgptsmscls  23654  ust0  23724  ustbas2  23730  iccntr  24337  pi1xfrcnv  24573  clsocv  24767  cfilfcls  24791  equivcmet  24834  hlhil  24960  evthicc2  24977  ovolshft  25028  volsup  25073  dyadmbllem  25116  mbfconstlem  25144  itg11  25208  limciun  25411  dvnres  25448  cpnord  25452  dvcmulf  25462  dvmptcmul  25481  dvcnvre  25536  plyco0  25706  taylthlem1  25885  taylthlem2  25886  ulmdvlem3  25914  wilthlem2  26573  ppisval  26608  ppinprm  26656  chtnprm  26658  sltval2  27159  noextenddif  27171  scutun12  27311  madebdaylemlrcut  27393  cofcut1  27407  negsbday  27531  upgrex  28352  uvtxnbgr  28657  cusgredg  28681  ubthlem1  30123  pjhth  30646  ococin  30661  chsupsn  30666  ssjo  30700  chabs1  30769  spansncvi  30905  mdslj1i  31572  mdslj2i  31573  atomli  31635  atcvatlem  31638  atcvat3i  31649  sumdmdlem  31671  difininv  31755  fnpreimac  31896  pmtrcnelor  32252  cycpmrn  32302  isdrng4  32395  fldgenid  32409  1fldgenq  32412  rspidlid  32487  0ringidl  32539  drngmxidl  32593  dimkerim  32712  algextdeglem1  32772  cmpcref  32830  zarcls1  32849  zarclssn  32853  zart0  32859  zarcmplem  32861  xpinpreima2  32887  ordtrest2NEW  32903  sigagenid  33149  imambfm  33261  reprinfz1  33634  bnj1136  34008  bnj1398  34045  bnj1408  34047  bnj1498  34072  fineqvacALT  34098  sconnpi1  34230  cvmliftlem15  34289  altopthsn  34933  opnbnd  35210  opnregcld  35215  cldregopn  35216  fnessref  35242  neibastop1  35244  topmeet  35249  topjoin  35250  fnemeet1  35251  fnejoin1  35253  bj-gabeqd  35817  bj-restpw  35973  bj-restb  35975  bj-restuni2  35979  dissneqlem  36221  pibt2  36298  lindsenlbs  36483  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  fdc  36613  sstotbnd2  36642  isbnd2  36651  totbndbnd  36657  prdstotbnd  36662  heibor1  36678  1idl  36894  igenval2  36934  idreseqidinxp  37178  disjdmqs  37674  lshpdisj  37857  lssats  37882  lsatcvat3  37922  lshpset2N  37989  lfl1dim  37991  lfl1dim2N  37992  lkrpssN  38033  paddass  38709  paddidm  38712  pmod1i  38719  pmapjat1  38724  pclbtwnN  38768  pclunN  38769  paddunN  38798  pclfinclN  38821  dihjust  40088  dihmeetlem1N  40161  dihglblem5apreN  40162  dihmeetlem13N  40190  dochocsp  40250  dochdmj1  40261  dochnoncon  40262  dihjatb  40287  dihjat1lem  40299  lcfl9a  40376  lclkrlem2s  40396  lclkrlem2v  40399  mapdrvallem3  40517  mapdunirnN  40521  mapdin  40533  mapdlsm  40535  baerlem3lem2  40581  baerlem5alem2  40582  baerlem5blem2  40583  hdmaplkr  40784  sticksstones11  40972  rntrclfvOAI  41429  ismrcd1  41436  ismrcd2  41437  isnacs3  41448  nacsfix  41450  rgspnid  41914  iocinico  41961  onsupmaxb  41988  onsssupeqcond  42030  oacl2g  42080  omabs2  42082  omcl2  42083  ofoaf  42105  onsucunifi  42120  naddwordnexlem4  42152  harval3  42289  mptrcllem  42364  clcnvlem  42374  dmtrcl  42378  rntrcl  42379  cbviuneq12df  42412  dfrcl2  42425  dftrcl3  42471  brtrclfv2  42478  dfrtrcl3  42484  scottrankd  43007  nzin  43077  iunincfi  43783  founiiun  43875  founiiun0  43888  inmap  43908  difmapsn  43911  funimaeq  43950  iuneqfzuz  44045  supminfrnmpt  44155  supminfxr2  44179  supminfxrrnmpt  44181  pimxrneun  44199  iooiinicc  44255  icomnfinre  44265  iooiinioc  44269  limsupresxr  44482  liminfresxr  44483  limsup10exlem  44488  liminfvalxr  44499  fourierdlem79  44901  rrxsnicc  45016  prsal  45034  issalgend  45054  sge0f1o  45098  caragenuni  45227  caragendifcl  45230  opnvonmbllem2  45349  iinhoiicc  45390  pimconstlt1  45418  pimltpnff  45419  pimiooltgt  45426  pimgtmnf2  45430  pimdecfgtioc  45431  pimincfltioc  45432  pimdecfgtioo  45433  pimincfltioo  45434  preimageiingt  45436  preimaleiinlt  45437  pimgtmnff  45438  sssmf  45454  smflimlem5  45491  smfmullem4  45510  smfpimbor1lem2  45515  smfsuplem1  45527  smfpimne2  45556  fsupdm  45558  finfdm  45562  fzoopth  46035  sprsymrelf1  46164  lspeqlco  47120  isclatd  47608  intubeu  47609  unilbeu  47610  setrecsres  47747