Theorem eqssd 3939

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

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

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 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  eqelssd  3943  uneqdifeq  4424  pweq  4550  unieq  4851  unissel  4873  intmin  4900  unissint  4904  int0el  4911  dmcosseq  5885  sofld  6095  relfld  6182  preddowncl  6239  frpoind  6249  wfiOLD  6258  tz7.7  6296  fimacnvOLD  6957  knatar  7237  sorpssuni  7594  sorpssint  7595  onint  7649  fo2ndf  7971  suppimacnv  7999  tposeq  8053  frrlem14  8124  onfununi  8181  tfrlem15  8232  oaass  8401  odi  8419  omass  8420  oelim2  8435  oeeui  8442  nnawordex  8477  oaabslem  8486  oaabs2  8488  omabslem  8489  omabs  8490  uniinqs  8595  sucdom2OLD  8878  sucdom2  8998  onomeneq  9020  fineqv  9047  dffi2  9191  fiuni  9196  dffi3  9199  hartogslem1  9310  ixpiunwdom  9358  cantnfp1lem3  9447  oemapvali  9451  cantnf  9460  dfttrcl2  9491  frind  9517  r1val1  9553  rankval3b  9593  rankunb  9617  rankuni2b  9620  rankr1id  9629  rankc2  9638  rankxplim  9646  tcrank  9651  carden2b  9734  harval2  9764  en2other2  9774  infpwfien  9827  coflim  10026  cfcof  10039  cfidm  10040  isf32lem2  10119  fin1a2lem11  10175  fin1a2lem13  10177  ttukeylem7  10280  fpwwe2  10408  winafp  10462  wuncidm  10511  wuncval2  10512  tskuni  10548  grur1  10585  distrpr  10793  ltexpri  10808  reclem4pr  10815  fzopth  13302  fzosplit  13429  fzouzsplit  13431  ccatrn  14303  cotrtrclfv  14732  dmtrclfv  14738  dfrtrcl2  14782  structcnvcnv  16863  imasaddfnlem  17248  imasvscafn  17257  mrcuni  17339  mressmrcd  17345  submrc  17346  ssceq  17547  rescabs  17556  rescabsOLD  17557  setcepi  17812  clatl  18235  ipopos  18263  psdmrn  18300  dirdm  18327  gsumress  18375  gsumvallem2  18481  gsumwspan  18494  trivsubgd  18790  trivsubgsnd  18791  trivnsgd  18809  cycsubg  18836  conjnmz  18877  pmtrprfv  19070  symggen  19087  odf1o2  19187  gex1  19205  sylow2alem1  19231  smndlsmidm  19270  lsmidmOLD  19278  lsmss1  19280  lsmss2  19282  lsmmod  19290  lsmdisj  19296  lsmdisj2  19297  cntzcmn  19450  prmcyg  19504  dmdprdd  19611  dprdspan  19639  dprdres  19640  dprdz  19642  subgdmdprd  19646  subgdprd  19647  dprddisj2  19651  dprd2dlem1  19653  dprd2da  19654  dmdprdsplit2lem  19657  dprdsplit  19660  ablfacrp  19678  pgpfac1lem3  19689  kerf1ghm  19996  issubdrg  20058  lspun  20258  lspsn  20273  lspsnneg  20277  lsp0  20280  lsslsp  20286  lmhmlsp  20320  lspextmo  20327  lsmsp  20357  lspprabs  20366  lspsnvs  20385  lspdisj  20396  lsmcv  20412  lspsnat  20416  lsppratlem6  20423  lspprat  20424  lbsextlem4  20432  lidl1el  20498  drngnidl  20509  lidldvgen  20535  cnsubrg  20667  mulgrhm2  20709  znrrg  20782  ocvin  20888  ocvlsp  20890  mrccss  20908  topsn  22089  eltg4i  22119  unitg  22126  tgtop  22132  tgidm  22139  en2top  22144  basgen  22147  2basgen  22149  fctop  22163  cctop  22165  ppttop  22166  epttop  22168  ntrin  22221  isopn3  22226  opnnei  22280  neiuni  22282  maxlp  22307  clslp  22308  tgrest  22319  resttopon  22321  rest0  22329  restcls  22341  restntr  22342  ordtbas2  22351  ordtbas  22352  ordtrest2  22364  cmpcov2  22550  tgcmp  22561  cmpcld  22562  uncmp  22563  cmpfi  22568  dis2ndc  22620  restnlly  22642  dislly  22657  comppfsc  22692  kgentopon  22698  kgencmp  22705  kgenidm  22707  iskgen2  22708  kgencn3  22718  ptuni2  22736  ptbasfi  22741  xkouni  22759  txcls  22764  txdis  22792  txindis  22794  txcmplem2  22802  xkopt  22815  txconn  22849  qtopval2  22856  qtopuni  22862  qtoprest  22877  qtopomap  22878  qtopcmap  22879  kqsat  22891  kqcldsat  22893  hmeocls  22928  hmeontr  22929  hmphdis  22956  fgfil  23035  fgabs  23039  trfil1  23046  fgtr  23050  uzrest  23057  ufilmax  23067  ufileu  23079  filufint  23080  ufildom1  23086  rnelfm  23113  flimfil  23129  uffclsflim  23191  alexsublem  23204  alexsubALTlem3  23209  alexsubALT  23211  ptcmplem2  23213  ptcmplem3  23214  tgpconncompeqg  23272  haustsms2  23297  tgptsmscls  23310  ust0  23380  ustbas2  23386  iccntr  23993  pi1xfrcnv  24229  clsocv  24423  cfilfcls  24447  equivcmet  24490  hlhil  24616  evthicc2  24633  ovolshft  24684  volsup  24729  dyadmbllem  24772  mbfconstlem  24800  itg11  24864  limciun  25067  dvnres  25104  cpnord  25108  dvcmulf  25118  dvmptcmul  25137  dvcnvre  25192  plyco0  25362  taylthlem1  25541  taylthlem2  25542  ulmdvlem3  25570  wilthlem2  26227  ppisval  26262  ppinprm  26310  chtnprm  26312  upgrex  27471  uvtxnbgr  27776  cusgredg  27800  ubthlem1  29241  pjhth  29764  ococin  29779  chsupsn  29784  ssjo  29818  chabs1  29887  spansncvi  30023  mdslj1i  30690  mdslj2i  30691  atomli  30753  atcvatlem  30756  atcvat3i  30767  sumdmdlem  30789  difininv  30873  fnpreimac  31017  pmtrcnelor  31369  cycpmrn  31419  rspidlid  31579  0ringidl  31614  dimkerim  31717  cmpcref  31809  zarcls1  31828  zarclssn  31832  zart0  31838  zarcmplem  31840  xpinpreima2  31866  ordtrest2NEW  31882  sigagenid  32128  imambfm  32238  reprinfz1  32611  bnj1136  32986  bnj1398  33023  bnj1408  33025  bnj1498  33050  fineqvacALT  33076  sconnpi1  33210  cvmliftlem15  33269  sltval2  33868  noextenddif  33880  scutun12  34013  madebdaylemlrcut  34088  cofcut1  34099  altopthsn  34272  opnbnd  34523  opnregcld  34528  cldregopn  34529  fnessref  34555  neibastop1  34557  topmeet  34562  topjoin  34563  fnemeet1  34564  fnejoin1  34566  bj-gabeqd  35134  bj-restpw  35272  bj-restb  35274  bj-restuni2  35278  dissneqlem  35520  pibt2  35597  lindsenlbs  35781  poimirlem13  35799  poimirlem14  35800  poimirlem15  35801  fdc  35912  sstotbnd2  35941  isbnd2  35950  totbndbnd  35956  prdstotbnd  35961  heibor1  35977  1idl  36193  igenval2  36233  idreseqidinxp  36452  lshpdisj  37008  lssats  37033  lsatcvat3  37073  lshpset2N  37140  lfl1dim  37142  lfl1dim2N  37143  lkrpssN  37184  paddass  37859  paddidm  37862  pmod1i  37869  pmapjat1  37874  pclbtwnN  37918  pclunN  37919  paddunN  37948  pclfinclN  37971  dihjust  39238  dihmeetlem1N  39311  dihglblem5apreN  39312  dihmeetlem13N  39340  dochocsp  39400  dochdmj1  39411  dochnoncon  39412  dihjatb  39437  dihjat1lem  39449  lcfl9a  39526  lclkrlem2s  39546  lclkrlem2v  39549  mapdrvallem3  39667  mapdunirnN  39671  mapdin  39683  mapdlsm  39685  baerlem3lem2  39731  baerlem5alem2  39732  baerlem5blem2  39733  hdmaplkr  39934  sticksstones11  40119  rntrclfvOAI  40520  ismrcd1  40527  ismrcd2  40528  isnacs3  40539  nacsfix  40541  rgspnid  41004  iocinico  41050  harval3  41152  mptrcllem  41228  clcnvlem  41238  dmtrcl  41242  rntrcl  41243  cbviuneq12df  41276  dfrcl2  41289  dftrcl3  41335  brtrclfv2  41342  dfrtrcl3  41348  scottrankd  41873  nzin  41943  iunincfi  42651  founiiun  42722  founiiun0  42735  inmap  42756  difmapsn  42759  funimaeq  42799  iuneqfzuz  42881  supminfrnmpt  42992  supminfxr2  43016  supminfxrrnmpt  43018  iooiinicc  43087  icomnfinre  43097  iooiinioc  43101  limsupresxr  43314  liminfresxr  43315  limsup10exlem  43320  liminfvalxr  43331  fourierdlem79  43733  rrxsnicc  43848  prsal  43866  issalgend  43884  sge0f1o  43927  caragenuni  44056  caragendifcl  44059  opnvonmbllem2  44178  iinhoiicc  44219  pimconstlt1  44247  pimltpnff  44248  pimiooltgt  44255  pimgtmnf2  44259  pimdecfgtioc  44260  pimincfltioc  44261  pimdecfgtioo  44262  pimincfltioo  44263  preimageiingt  44265  preimaleiinlt  44266  pimgtmnff  44267  sssmf  44283  smflimlem5  44320  smfmullem4  44339  smfpimbor1lem2  44344  smfsuplem1  44355  fzoopth  44830  sprsymrelf1  44959  lspeqlco  45791  isclatd  46280  intubeu  46281  unilbeu  46282  setrecsres  46418