Theorem eqssd 3984

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  eqelssd  3988  uneqdifeq  4438  pweq  4555  unieq  4849  unissel  4869  intmin  4896  unissint  4900  int0el  4907  dmcosseq  5844  sofld  6044  relfld  6126  preddowncl  6175  wfi  6181  tz7.7  6217  fimacnv  6839  knatar  7110  sorpssuni  7458  sorpssint  7459  onint  7510  fo2ndf  7817  suppimacnv  7841  tposeq  7894  onfununi  7978  tfrlem15  8028  oaass  8187  odi  8205  omass  8206  oelim2  8221  oeeui  8228  nnawordex  8263  oaabslem  8270  oaabs2  8272  omabslem  8273  omabs  8274  uniinqs  8377  sucdom2  8714  fineqv  8733  dffi2  8887  fiuni  8892  dffi3  8895  hartogslem1  9006  ixpiunwdom  9055  cantnfp1lem3  9143  oemapvali  9147  cantnf  9156  r1val1  9215  rankval3b  9255  rankunb  9279  rankuni2b  9282  rankr1id  9291  rankc2  9300  rankxplim  9308  tcrank  9313  carden2b  9396  harval2  9426  en2other2  9435  infpwfien  9488  coflim  9683  cfcof  9696  cfidm  9697  isf32lem2  9776  fin1a2lem11  9832  fin1a2lem13  9834  ttukeylem7  9937  fpwwe2  10065  winafp  10119  wuncidm  10168  wuncval2  10169  tskuni  10205  grur1  10242  distrpr  10450  ltexpri  10465  reclem4pr  10472  fzopth  12945  fzosplit  13071  fzouzsplit  13073  ccatrn  13943  cotrtrclfv  14372  dmtrclfv  14378  dfrtrcl2  14421  structcnvcnv  16497  imasaddfnlem  16801  imasvscafn  16810  mrcuni  16892  mressmrcd  16898  submrc  16899  ssceq  17096  rescabs  17103  setcepi  17348  clatl  17726  ipopos  17770  psdmrn  17817  dirdm  17844  gsumress  17892  gsumvallem2  17998  gsumwspan  18011  trivsubgd  18305  trivsubgsnd  18306  trivnsgd  18324  cycsubg  18351  conjnmz  18392  pmtrprfv  18581  symggen  18598  odf1o2  18698  gex1  18716  sylow2alem1  18742  smndlsmidm  18781  lsmidmOLD  18789  lsmss1  18791  lsmss2  18793  lsmmod  18801  lsmdisj  18807  lsmdisj2  18808  cntzcmn  18960  prmcyg  19014  dmdprdd  19121  dprdspan  19149  dprdres  19150  dprdz  19152  subgdmdprd  19156  subgdprd  19157  dprddisj2  19161  dprd2dlem1  19163  dprd2da  19164  dmdprdsplit2lem  19167  dprdsplit  19170  ablfacrp  19188  pgpfac1lem3  19199  kerf1ghm  19497  kerf1hrmOLD  19498  issubdrg  19560  lspun  19759  lspsn  19774  lspsnneg  19778  lsp0  19781  lsslsp  19787  lmhmlsp  19821  lspextmo  19828  lsmsp  19858  lspprabs  19867  lspsnvs  19886  lspdisj  19897  lsmcv  19913  lspsnat  19917  lsppratlem6  19924  lspprat  19925  lbsextlem4  19933  lidl1el  19991  drngnidl  20002  lidldvgen  20028  cnsubrg  20605  mulgrhm2  20646  znrrg  20712  ocvin  20818  ocvlsp  20820  mrccss  20838  topsn  21539  eltg4i  21568  unitg  21575  tgtop  21581  tgidm  21588  en2top  21593  basgen  21596  2basgen  21598  fctop  21612  cctop  21614  ppttop  21615  epttop  21617  ntrin  21669  isopn3  21674  opnnei  21728  neiuni  21730  maxlp  21755  clslp  21756  tgrest  21767  resttopon  21769  rest0  21777  restcls  21789  restntr  21790  ordtbas2  21799  ordtbas  21800  ordtrest2  21812  cmpcov2  21998  tgcmp  22009  cmpcld  22010  uncmp  22011  cmpfi  22016  dis2ndc  22068  restnlly  22090  dislly  22105  comppfsc  22140  kgentopon  22146  kgencmp  22153  kgenidm  22155  iskgen2  22156  kgencn3  22166  ptuni2  22184  ptbasfi  22189  xkouni  22207  txcls  22212  txdis  22240  txindis  22242  txcmplem2  22250  xkopt  22263  txconn  22297  qtopval2  22304  qtopuni  22310  qtoprest  22325  qtopomap  22326  qtopcmap  22327  kqsat  22339  kqcldsat  22341  hmeocls  22376  hmeontr  22377  hmphdis  22404  fgfil  22483  fgabs  22487  trfil1  22494  fgtr  22498  uzrest  22505  ufilmax  22515  ufileu  22527  filufint  22528  ufildom1  22534  rnelfm  22561  flimfil  22577  uffclsflim  22639  alexsublem  22652  alexsubALTlem3  22657  alexsubALT  22659  ptcmplem2  22661  ptcmplem3  22662  tgpconncompeqg  22720  haustsms2  22745  tgptsmscls  22758  ust0  22828  ustbas2  22834  iccntr  23429  pi1xfrcnv  23661  clsocv  23853  cfilfcls  23877  equivcmet  23920  hlhil  24046  evthicc2  24061  ovolshft  24112  volsup  24157  dyadmbllem  24200  mbfconstlem  24228  itg11  24292  limciun  24492  dvnres  24528  cpnord  24532  dvcmulf  24542  dvmptcmul  24561  dvcnvre  24616  plyco0  24782  taylthlem1  24961  taylthlem2  24962  ulmdvlem3  24990  wilthlem2  25646  ppisval  25681  ppinprm  25729  chtnprm  25731  upgrex  26877  uvtxnbgr  27182  cusgredg  27206  ubthlem1  28647  pjhth  29170  ococin  29185  chsupsn  29190  ssjo  29224  chabs1  29293  spansncvi  29429  mdslj1i  30096  mdslj2i  30097  atomli  30159  atcvatlem  30162  atcvat3i  30173  sumdmdlem  30195  difininv  30279  fnpreimac  30416  pmtrcnelor  30735  cycpmrn  30785  dimkerim  31023  cmpcref  31114  xpinpreima2  31150  ordtrest2NEW  31166  sigagenid  31410  imambfm  31520  reprinfz1  31893  bnj1136  32269  bnj1398  32306  bnj1408  32308  bnj1498  32333  sconnpi1  32486  cvmliftlem15  32545  dftrpred3g  33072  trpredpo  33074  frpoind  33080  frind  33085  frrlem14  33136  sltval2  33163  noextenddif  33175  scutun12  33271  altopthsn  33422  opnbnd  33673  opnregcld  33678  cldregopn  33679  fnessref  33705  neibastop1  33707  topmeet  33712  topjoin  33713  fnemeet1  33714  fnejoin1  33716  bj-restpw  34386  bj-restb  34388  bj-restuni2  34392  dissneqlem  34624  pibt2  34701  lindsenlbs  34902  poimirlem13  34920  poimirlem14  34921  poimirlem15  34922  fdc  35035  sstotbnd2  35067  isbnd2  35076  totbndbnd  35082  prdstotbnd  35087  heibor1  35103  1idl  35319  igenval2  35359  idreseqidinxp  35582  lshpdisj  36138  lssats  36163  lsatcvat3  36203  lshpset2N  36270  lfl1dim  36272  lfl1dim2N  36273  lkrpssN  36314  paddass  36989  paddidm  36992  pmod1i  36999  pmapjat1  37004  pclbtwnN  37048  pclunN  37049  paddunN  37078  pclfinclN  37101  dihjust  38368  dihmeetlem1N  38441  dihglblem5apreN  38442  dihmeetlem13N  38470  dochocsp  38530  dochdmj1  38541  dochnoncon  38542  dihjatb  38567  dihjat1lem  38579  lcfl9a  38656  lclkrlem2s  38676  lclkrlem2v  38679  mapdrvallem3  38797  mapdunirnN  38801  mapdin  38813  mapdlsm  38815  baerlem3lem2  38861  baerlem5alem2  38862  baerlem5blem2  38863  hdmaplkr  39064  rntrclfvOAI  39337  ismrcd1  39344  ismrcd2  39345  isnacs3  39356  nacsfix  39358  rgspnid  39821  iocinico  39867  harval3  39953  mptrcllem  40022  clcnvlem  40032  dmtrcl  40036  rntrcl  40037  cbviuneq12df  40055  dfrcl2  40068  dftrcl3  40114  brtrclfv2  40121  dfrtrcl3  40127  scottrankd  40633  nzin  40699  iunincfi  41409  founiiun  41484  founiiun0  41500  inmap  41521  difmapsn  41524  funimaeq  41567  iuneqfzuz  41652  supminfrnmpt  41768  supminfxr2  41794  supminfxrrnmpt  41796  iooiinicc  41867  icomnfinre  41877  iooiinioc  41881  limsupresxr  42096  liminfresxr  42097  limsup10exlem  42102  liminfvalxr  42113  fourierdlem79  42519  rrxsnicc  42634  prsal  42652  issalgend  42670  sge0f1o  42713  caragenuni  42842  caragendifcl  42845  opnvonmbllem2  42964  iinhoiicc  43005  pimconstlt1  43032  pimltpnf  43033  pimiooltgt  43038  pimgtmnf2  43041  pimdecfgtioc  43042  pimincfltioc  43043  pimdecfgtioo  43044  pimincfltioo  43045  preimageiingt  43047  preimaleiinlt  43048  sssmf  43064  smflimlem5  43100  smfmullem4  43118  smfpimbor1lem2  43123  smfsuplem1  43134  fzoopth  43576  sprsymrelf1  43707  lspeqlco  44543  setrecsres  44853