Theorem eqssd 3934

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  eqelssd  3938  uneqdifeq  4420  pweq  4546  unieq  4847  unissel  4869  intmin  4896  unissint  4900  int0el  4907  dmcosseq  5871  sofld  6079  relfld  6167  preddowncl  6224  frpoind  6230  wfiOLD  6239  tz7.7  6277  fimacnvOLD  6930  knatar  7208  sorpssuni  7563  sorpssint  7564  onint  7617  fo2ndf  7933  suppimacnv  7961  tposeq  8015  frrlem14  8086  onfununi  8143  tfrlem15  8194  oaass  8354  odi  8372  omass  8373  oelim2  8388  oeeui  8395  nnawordex  8430  oaabslem  8437  oaabs2  8439  omabslem  8440  omabs  8441  uniinqs  8544  sucdom2  8822  fineqv  8967  dffi2  9112  fiuni  9117  dffi3  9120  hartogslem1  9231  ixpiunwdom  9279  cantnfp1lem3  9368  oemapvali  9372  cantnf  9381  dftrpred3g  9412  trpredpo  9414  frind  9439  r1val1  9475  rankval3b  9515  rankunb  9539  rankuni2b  9542  rankr1id  9551  rankc2  9560  rankxplim  9568  tcrank  9573  carden2b  9656  harval2  9686  en2other2  9696  infpwfien  9749  coflim  9948  cfcof  9961  cfidm  9962  isf32lem2  10041  fin1a2lem11  10097  fin1a2lem13  10099  ttukeylem7  10202  fpwwe2  10330  winafp  10384  wuncidm  10433  wuncval2  10434  tskuni  10470  grur1  10507  distrpr  10715  ltexpri  10730  reclem4pr  10737  fzopth  13222  fzosplit  13348  fzouzsplit  13350  ccatrn  14222  cotrtrclfv  14651  dmtrclfv  14657  dfrtrcl2  14701  structcnvcnv  16782  imasaddfnlem  17156  imasvscafn  17165  mrcuni  17247  mressmrcd  17253  submrc  17254  ssceq  17455  rescabs  17464  setcepi  17719  clatl  18141  ipopos  18169  psdmrn  18206  dirdm  18233  gsumress  18281  gsumvallem2  18387  gsumwspan  18400  trivsubgd  18696  trivsubgsnd  18697  trivnsgd  18715  cycsubg  18742  conjnmz  18783  pmtrprfv  18976  symggen  18993  odf1o2  19093  gex1  19111  sylow2alem1  19137  smndlsmidm  19176  lsmidmOLD  19184  lsmss1  19186  lsmss2  19188  lsmmod  19196  lsmdisj  19202  lsmdisj2  19203  cntzcmn  19356  prmcyg  19410  dmdprdd  19517  dprdspan  19545  dprdres  19546  dprdz  19548  subgdmdprd  19552  subgdprd  19553  dprddisj2  19557  dprd2dlem1  19559  dprd2da  19560  dmdprdsplit2lem  19563  dprdsplit  19566  ablfacrp  19584  pgpfac1lem3  19595  kerf1ghm  19902  issubdrg  19964  lspun  20164  lspsn  20179  lspsnneg  20183  lsp0  20186  lsslsp  20192  lmhmlsp  20226  lspextmo  20233  lsmsp  20263  lspprabs  20272  lspsnvs  20291  lspdisj  20302  lsmcv  20318  lspsnat  20322  lsppratlem6  20329  lspprat  20330  lbsextlem4  20338  lidl1el  20402  drngnidl  20413  lidldvgen  20439  cnsubrg  20570  mulgrhm2  20612  znrrg  20685  ocvin  20791  ocvlsp  20793  mrccss  20811  topsn  21988  eltg4i  22018  unitg  22025  tgtop  22031  tgidm  22038  en2top  22043  basgen  22046  2basgen  22048  fctop  22062  cctop  22064  ppttop  22065  epttop  22067  ntrin  22120  isopn3  22125  opnnei  22179  neiuni  22181  maxlp  22206  clslp  22207  tgrest  22218  resttopon  22220  rest0  22228  restcls  22240  restntr  22241  ordtbas2  22250  ordtbas  22251  ordtrest2  22263  cmpcov2  22449  tgcmp  22460  cmpcld  22461  uncmp  22462  cmpfi  22467  dis2ndc  22519  restnlly  22541  dislly  22556  comppfsc  22591  kgentopon  22597  kgencmp  22604  kgenidm  22606  iskgen2  22607  kgencn3  22617  ptuni2  22635  ptbasfi  22640  xkouni  22658  txcls  22663  txdis  22691  txindis  22693  txcmplem2  22701  xkopt  22714  txconn  22748  qtopval2  22755  qtopuni  22761  qtoprest  22776  qtopomap  22777  qtopcmap  22778  kqsat  22790  kqcldsat  22792  hmeocls  22827  hmeontr  22828  hmphdis  22855  fgfil  22934  fgabs  22938  trfil1  22945  fgtr  22949  uzrest  22956  ufilmax  22966  ufileu  22978  filufint  22979  ufildom1  22985  rnelfm  23012  flimfil  23028  uffclsflim  23090  alexsublem  23103  alexsubALTlem3  23108  alexsubALT  23110  ptcmplem2  23112  ptcmplem3  23113  tgpconncompeqg  23171  haustsms2  23196  tgptsmscls  23209  ust0  23279  ustbas2  23285  iccntr  23890  pi1xfrcnv  24126  clsocv  24319  cfilfcls  24343  equivcmet  24386  hlhil  24512  evthicc2  24529  ovolshft  24580  volsup  24625  dyadmbllem  24668  mbfconstlem  24696  itg11  24760  limciun  24963  dvnres  25000  cpnord  25004  dvcmulf  25014  dvmptcmul  25033  dvcnvre  25088  plyco0  25258  taylthlem1  25437  taylthlem2  25438  ulmdvlem3  25466  wilthlem2  26123  ppisval  26158  ppinprm  26206  chtnprm  26208  upgrex  27365  uvtxnbgr  27670  cusgredg  27694  ubthlem1  29133  pjhth  29656  ococin  29671  chsupsn  29676  ssjo  29710  chabs1  29779  spansncvi  29915  mdslj1i  30582  mdslj2i  30583  atomli  30645  atcvatlem  30648  atcvat3i  30659  sumdmdlem  30681  difininv  30765  fnpreimac  30910  pmtrcnelor  31262  cycpmrn  31312  rspidlid  31472  0ringidl  31507  dimkerim  31610  cmpcref  31702  zarcls1  31721  zarclssn  31725  zart0  31731  zarcmplem  31733  xpinpreima2  31759  ordtrest2NEW  31775  sigagenid  32019  imambfm  32129  reprinfz1  32502  bnj1136  32877  bnj1398  32914  bnj1408  32916  bnj1498  32941  fineqvacALT  32967  sconnpi1  33101  cvmliftlem15  33160  dfttrcl2  33710  sltval2  33786  noextenddif  33798  scutun12  33931  madebdaylemlrcut  34006  cofcut1  34017  altopthsn  34190  opnbnd  34441  opnregcld  34446  cldregopn  34447  fnessref  34473  neibastop1  34475  topmeet  34480  topjoin  34481  fnemeet1  34482  fnejoin1  34484  bj-gabeqd  35052  bj-restpw  35190  bj-restb  35192  bj-restuni2  35196  dissneqlem  35438  pibt2  35515  lindsenlbs  35699  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  fdc  35830  sstotbnd2  35859  isbnd2  35868  totbndbnd  35874  prdstotbnd  35879  heibor1  35895  1idl  36111  igenval2  36151  idreseqidinxp  36372  lshpdisj  36928  lssats  36953  lsatcvat3  36993  lshpset2N  37060  lfl1dim  37062  lfl1dim2N  37063  lkrpssN  37104  paddass  37779  paddidm  37782  pmod1i  37789  pmapjat1  37794  pclbtwnN  37838  pclunN  37839  paddunN  37868  pclfinclN  37891  dihjust  39158  dihmeetlem1N  39231  dihglblem5apreN  39232  dihmeetlem13N  39260  dochocsp  39320  dochdmj1  39331  dochnoncon  39332  dihjatb  39357  dihjat1lem  39369  lcfl9a  39446  lclkrlem2s  39466  lclkrlem2v  39469  mapdrvallem3  39587  mapdunirnN  39591  mapdin  39603  mapdlsm  39605  baerlem3lem2  39651  baerlem5alem2  39652  baerlem5blem2  39653  hdmaplkr  39854  sticksstones11  40040  rntrclfvOAI  40429  ismrcd1  40436  ismrcd2  40437  isnacs3  40448  nacsfix  40450  rgspnid  40913  iocinico  40959  harval3  41041  mptrcllem  41110  clcnvlem  41120  dmtrcl  41124  rntrcl  41125  cbviuneq12df  41158  dfrcl2  41171  dftrcl3  41217  brtrclfv2  41224  dfrtrcl3  41230  scottrankd  41755  nzin  41825  iunincfi  42533  founiiun  42604  founiiun0  42617  inmap  42638  difmapsn  42641  funimaeq  42681  iuneqfzuz  42764  supminfrnmpt  42875  supminfxr2  42899  supminfxrrnmpt  42901  iooiinicc  42970  icomnfinre  42980  iooiinioc  42984  limsupresxr  43197  liminfresxr  43198  limsup10exlem  43203  liminfvalxr  43214  fourierdlem79  43616  rrxsnicc  43731  prsal  43749  issalgend  43767  sge0f1o  43810  caragenuni  43939  caragendifcl  43942  opnvonmbllem2  44061  iinhoiicc  44102  pimconstlt1  44129  pimltpnf  44130  pimiooltgt  44135  pimgtmnf2  44138  pimdecfgtioc  44139  pimincfltioc  44140  pimdecfgtioo  44141  pimincfltioo  44142  preimageiingt  44144  preimaleiinlt  44145  sssmf  44161  smflimlem5  44197  smfmullem4  44215  smfpimbor1lem2  44220  smfsuplem1  44231  fzoopth  44707  sprsymrelf1  44836  lspeqlco  45668  isclatd  46157  intubeu  46158  unilbeu  46159  setrecsres  46293