Theorem eqssd 3948

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2752  df-ss 3916

This theorem is used by:  eqelssd  3952  uneqdifeq  4448  pweq  4571  unieq  4878  unissel  4900  intmin  4928  unissint  4932  int0el  4939  intidg  5432  dmcosseq  5962  dmcosseqOLD  5963  sofld  6180  imadifssran  6197  imadifssranOLD  6198  relfld  6272  preddowncl  6330  frpoind  6340  tz7.7  6383  knatar  7361  sorpssuni  7734  sorpssint  7735  onint  7790  fo2ndf  8119  suppimacnv  8173  tposeq  8227  frrlem14  8299  onfununi  8331  tfrlem15  8382  oaass  8551  odi  8569  omass  8570  oelim2  8586  oeeui  8593  nnawordex  8628  oaabslem  8638  oaabs2  8640  omabslem  8641  omabs  8642  cofon1  8663  uniinqs  8800  sucdom2  9200  onomeneq  9211  fineqv  9240  dffi2  9396  fiuni  9401  dffi3  9404  hartogslem1  9517  ixpiunwdom  9565  cantnfp1lem3  9662  oemapvali  9666  cantnf  9675  dfttrcl2  9706  frind  9735  r1val1  9771  rankval3b  9811  rankunb  9835  rankuni2b  9838  rankr1id  9847  rankc2  9856  rankxplim  9864  tcrank  9869  scottrankd  9891  carden2b  9975  harval2  10005  en2other2  10015  infpwfien  10068  coflim  10266  cfcof  10279  cfidm  10280  isf32lem2  10359  fin1a2lem11  10415  fin1a2lem13  10417  ttukeylem7  10520  fpwwe2  10655  winafp  10709  wuncidm  10758  wuncval2  10759  tskuni  10795  grur1  10832  distrpr  11040  ltexpri  11055  reclem4pr  11062  fzopth  13619  fzosplit  13751  fzouzsplit  13753  fzoopth  13821  ccatrn  14658  cotrtrclfv  15088  dmtrclfv  15094  dfrtrcl2  15138  structcnvcnv  17248  imasaddfnlem  17617  imasvscafn  17626  mrcuni  17712  mressmrcd  17718  submrc  17719  ssceq  17918  rescabs  17925  setcepi  18180  clatl  18599  ipopos  18627  psdmrn  18664  dirdm  18691  gsumress  18787  gsumvallem2  18946  gsumwspan  18958  trivsubgd  19279  trivsubgsnd  19280  trivnsgd  19298  cycsubg  19339  kerf1ghm  19377  conjnmz  19382  pmtrprfv  19583  symggen  19600  odf1o2  19703  gex1  19721  sylow2alem1  19747  smndlsmidm  19786  lsmss1  19795  lsmss2  19797  lsmmod  19805  lsmdisj  19811  lsmdisj2  19812  cntzcmn  19970  prmcyg  20024  dmdprdd  20131  dprdspan  20159  dprdres  20160  dprdz  20162  subgdmdprd  20166  subgdprd  20167  dprddisj2  20171  dprd2dlem1  20173  dprd2da  20174  dmdprdsplit2lem  20177  dprdsplit  20180  ablfacrp  20198  pgpfac1lem3  20209  isdrng4  20905  issubdrg  20949  lspun  21174  lspsn  21189  lspsnneg  21193  lsp0  21196  lsslsp  21202  lmhmlsp  21236  lspextmo  21243  lsmsp  21273  lspprabs  21282  lspsnvs  21304  lspdisj  21315  lsmcv  21331  lspsnat  21335  lsppratlem6  21342  lspprat  21343  lbsextlem4  21351  lidl1el  21417  0ringidl  21426  rspprop  21436  drngnidl  21443  lidldvgen  21568  cnsubrg  21643  mulgrhm2  21694  znrrg  21781  ocvin  21890  ocvlsp  21892  mrccss  21910  lindsenlbs  22067  topsn  23159  eltg4i  23188  unitg  23195  tgtop  23201  tgidm  23208  en2top  23213  basgen  23216  2basgen  23218  fctop  23232  cctop  23234  ppttop  23235  epttop  23237  ntrin  23289  isopn3  23294  opnnei  23348  neiuni  23350  maxlp  23375  clslp  23376  tgrest  23387  resttopon  23389  rest0  23397  restcls  23409  restntr  23410  ordtbas2  23419  ordtbas  23420  ordtrest2  23432  cmpcov2  23618  tgcmp  23629  cmpcld  23630  uncmp  23631  cmpfi  23636  dis2ndc  23689  restnlly  23711  dislly  23726  comppfsc  23761  kgentopon  23767  kgencmp  23774  kgenidm  23776  iskgen2  23777  kgencn3  23787  ptuni2  23805  ptbasfi  23810  xkouni  23828  txcls  23833  txdis  23861  txindis  23863  txcmplem2  23871  xkopt  23884  txconn  23918  qtopval2  23925  qtopuni  23931  qtoprest  23946  qtopomap  23947  qtopcmap  23948  kqsat  23960  kqcldsat  23962  hmeocls  23997  hmeontr  23998  hmphdis  24025  fgfil  24104  fgabs  24108  trfil1  24115  fgtr  24119  uzrest  24126  ufilmax  24136  ufileu  24148  filufint  24149  ufildom1  24155  rnelfm  24182  flimfil  24198  uffclsflim  24260  alexsublem  24273  alexsubALTlem3  24278  alexsubALT  24280  ptcmplem2  24282  ptcmplem3  24283  tgpconncompeqg  24341  haustsms2  24366  tgptsmscls  24379  ust0  24449  ustbas2  24454  iccntr  25051  pi1xfrcnv  25288  clsocv  25481  cfilfcls  25505  equivcmet  25548  hlhil  25674  evthicc2  25691  ovolshft  25742  volsup  25787  dyadmbllem  25830  mbfconstlem  25858  itg11  25922  limciun  26124  dvnres  26161  cpnord  26165  dvcmulf  26175  dvmptcmul  26194  dvcnvre  26249  plyco0  26420  taylthlem1  26612  taylthlem2  26613  ulmdvlem3  26641  wilthlem2  27308  ppisval  27343  ppinprm  27391  chtnprm  27393  ltsval2  27895  noextenddif  27907  cutsun12  28058  madebdaylemlrcut  28167  bdayiun  28183  cofcut1  28188  negbday  28325  oniso  28539  bdayons  28544  addonbday  28547  bdayn0p1  28637  plngrot  29150  upgrex  29552  uvtxnbgr  29863  cusgredg  29887  ubthlem1  31354  pjhth  31877  ococin  31892  chsupsn  31897  ssjo  31931  chabs1  32000  spansncvi  32136  mdslj1i  32803  mdslj2i  32804  atomli  32866  atcvatlem  32869  atcvat3i  32880  sumdmdlem  32902  difininv  32995  fnpreimac  33146  pmtrcnelor  33534  cycpmrn  33586  elrgspnlem4  33688  fldgenid  33763  1fldgenq  33766  rspidlid  33812  drngmxidl  33882  drngmxidlr  33883  esplyfvaln  34087  resssra  34100  dimkerim  34140  fldextrspunlem1  34188  fldextrspunlem2  34190  algextdeglem4  34233  cmpcref  34363  zarcls1  34382  zarclssn  34386  zart0  34392  zarcmplem  34394  xpinpreima2  34420  ordtrest2NEW  34436  sigagenid  34665  imambfm  34776  reprinfz1  35133  bnj1136  35509  bnj1398  35546  bnj1408  35548  bnj1498  35573  rankval4b  35610  r1omhfb  35625  elscottrankeq  35632  fineqvacALT  35646  r1omhfbregs  35666  vonf1oonfo  35715  sconnpi1  35821  cvmliftlem15  35880  altopthsn  36544  nadddi  36807  opnbnd  36947  opnregcld  36952  cldregopn  36953  fnessref  36979  neibastop1  36981  topmeet  36986  topjoin  36987  fnemeet1  36988  fnejoin1  36990  ttctrid  37124  dfttc2g  37128  dfttc3gw  37145  bj-gabeqd  37684  bj-restpw  37845  bj-restb  37847  bj-restuni2  37851  dissneqlem  38097  pibt2  38174  poimirlem13  38385  poimirlem14  38386  poimirlem15  38387  fdc  38498  sstotbnd2  38527  isbnd2  38536  totbndbnd  38542  prdstotbnd  38547  heibor1  38563  1idl  38779  igenval2  38819  idreseqidinxp  39066  disjdmqs  39658  lshpdisj  39863  lssats  39888  lsatcvat3  39928  lshpset2N  39995  lfl1dim  39997  lfl1dim2N  39998  lkrpssN  40039  paddass  40714  paddidm  40717  pmod1i  40724  pmapjat1  40729  pclbtwnN  40773  pclunN  40774  paddunN  40803  pclfinclN  40826  dihjust  42093  dihmeetlem1N  42166  dihglblem5apreN  42167  dihmeetlem13N  42195  dochocsp  42255  dochdmj1  42266  dochnoncon  42267  dihjatb  42292  dihjat1lem  42304  lcfl9a  42381  lclkrlem2s  42401  lclkrlem2v  42404  mapdrvallem3  42522  mapdunirnN  42526  mapdin  42538  mapdlsm  42540  baerlem3lem2  42586  baerlem5alem2  42587  baerlem5blem2  42588  hdmaplkr  42789  primrootsunit1  42966  sticksstones11  43025  aks6d1c6lem5  43046  unitscyglem4  43067  rntrclfvOAI  43539  ismrcd1  43546  ismrcd2  43547  isnacs3  43558  nacsfix  43560  rgspnid  44012  iocinico  44056  onsupmaxb  44083  onsssupeqcond  44124  oacl2g  44174  omabs2  44176  omcl2  44177  ofoaf  44199  onsucunifi  44214  naddwordnexlem4  44245  harval3  44381  mptrcllem  44456  clcnvlem  44466  dmtrcl  44470  rntrcl  44471  cbviuneq12df  44504  dfrcl2  44517  dftrcl3  44563  brtrclfv2  44570  dfrtrcl3  44576  nzin  45145  iunincfi  45929  founiiun  46014  founiiun0  46025  inmap  46042  difmapsn  46045  funimaeq  46078  iuneqfzuz  46168  supminfrnmpt  46276  supminfxr2  46300  supminfxrrnmpt  46302  pimxrneun  46319  iooiinicc  46375  icomnfinre  46385  iooiinioc  46389  limsupresxr  46597  liminfresxr  46598  limsup10exlem  46603  liminfvalxr  46614  fourierdlem79  47016  rrxsnicc  47131  prsal  47149  issalgend  47169  sge0f1o  47213  caragenuni  47342  caragendifcl  47345  opnvonmbllem2  47464  iinhoiicc  47505  pimconstlt1  47533  pimltpnff  47534  pimiooltgt  47541  pimgtmnf2  47545  pimdecfgtioc  47546  pimincfltioc  47547  pimdecfgtioo  47548  pimincfltioo  47549  preimageiingt  47551  preimaleiinlt  47552  pimgtmnff  47553  sssmf  47569  smflimlem5  47606  smfmullem4  47625  smfpimbor1lem2  47630  smfsuplem1  47642  smfpimne2  47671  fsupdm  47673  finfdm  47677  tmachlem-agreesn  47778  sprsymrelf1  48399  lspeqlco  49372  iunlub  49752  iinglb  49753  iuneqconst2  49754  iineqconst2  49755  isclatd  49912  intubeu  49913  unilbeu  49914  setrecsres  50631