Theorem eqssd 3955

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

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

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 2156  ax-ext 2737

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

This theorem is used by:  eqelssd  3959  uneqdifeq  4455  pweq  4578  unieq  4885  unissel  4907  intmin  4935  unissint  4939  int0el  4946  intidg  5440  dmcosseq  5970  dmcosseqOLD  5971  sofld  6187  imadifssran  6204  imadifssranOLD  6205  relfld  6279  preddowncl  6337  frpoind  6347  tz7.7  6390  knatar  7366  sorpssuni  7739  sorpssint  7740  onint  7795  fo2ndf  8122  suppimacnv  8176  tposeq  8230  frrlem14  8302  onfununi  8334  tfrlem15  8385  oaass  8552  odi  8570  omass  8571  oelim2  8587  oeeui  8594  nnawordex  8629  oaabslem  8639  oaabs2  8641  omabslem  8642  omabs  8643  cofon1  8664  uniinqs  8801  sucdom2  9194  onomeneq  9205  fineqv  9234  dffi2  9390  fiuni  9395  dffi3  9398  hartogslem1  9511  ixpiunwdom  9559  cantnfp1lem3  9656  oemapvali  9660  cantnf  9669  dfttrcl2  9700  frind  9729  r1val1  9765  rankval3b  9805  rankunb  9829  rankuni2b  9832  rankr1id  9841  rankc2  9850  rankxplim  9858  tcrank  9863  scottrankd  9885  carden2b  9969  harval2  9999  en2other2  10009  infpwfien  10062  coflim  10260  cfcof  10273  cfidm  10274  isf32lem2  10353  fin1a2lem11  10409  fin1a2lem13  10411  ttukeylem7  10514  fpwwe2  10645  winafp  10699  wuncidm  10748  wuncval2  10749  tskuni  10785  grur1  10822  distrpr  11030  ltexpri  11045  reclem4pr  11052  fzopth  13608  fzosplit  13740  fzouzsplit  13742  fzoopth  13810  ccatrn  14647  cotrtrclfv  15075  dmtrclfv  15081  dfrtrcl2  15125  structcnvcnv  17237  imasaddfnlem  17606  imasvscafn  17615  mrcuni  17701  mressmrcd  17707  submrc  17708  ssceq  17907  rescabs  17914  setcepi  18169  clatl  18588  ipopos  18616  psdmrn  18653  dirdm  18680  gsumress  18774  gsumvallem2  18932  gsumwspan  18944  trivsubgd  19265  trivsubgsnd  19266  trivnsgd  19284  cycsubg  19325  kerf1ghm  19363  conjnmz  19368  pmtrprfv  19569  symggen  19586  odf1o2  19689  gex1  19707  sylow2alem1  19733  smndlsmidm  19772  lsmss1  19781  lsmss2  19783  lsmmod  19791  lsmdisj  19797  lsmdisj2  19798  cntzcmn  19956  prmcyg  20010  dmdprdd  20117  dprdspan  20145  dprdres  20146  dprdz  20148  subgdmdprd  20152  subgdprd  20153  dprddisj2  20157  dprd2dlem1  20159  dprd2da  20160  dmdprdsplit2lem  20163  dprdsplit  20166  ablfacrp  20184  pgpfac1lem3  20195  isdrng4  20891  issubdrg  20935  lspun  21160  lspsn  21175  lspsnneg  21179  lsp0  21182  lsslsp  21188  lmhmlsp  21222  lspextmo  21229  lsmsp  21259  lspprabs  21268  lspsnvs  21290  lspdisj  21301  lsmcv  21317  lspsnat  21321  lsppratlem6  21328  lspprat  21329  lbsextlem4  21337  lidl1el  21403  0ringidl  21412  rspprop  21422  drngnidl  21429  lidldvgen  21554  cnsubrg  21629  mulgrhm2  21680  znrrg  21767  ocvin  21876  ocvlsp  21878  mrccss  21896  topsn  23140  eltg4i  23169  unitg  23176  tgtop  23182  tgidm  23189  en2top  23194  basgen  23197  2basgen  23199  fctop  23213  cctop  23215  ppttop  23216  epttop  23218  ntrin  23270  isopn3  23275  opnnei  23329  neiuni  23331  maxlp  23356  clslp  23357  tgrest  23368  resttopon  23370  rest0  23378  restcls  23390  restntr  23391  ordtbas2  23400  ordtbas  23401  ordtrest2  23413  cmpcov2  23599  tgcmp  23610  cmpcld  23611  uncmp  23612  cmpfi  23617  dis2ndc  23670  restnlly  23692  dislly  23707  comppfsc  23742  kgentopon  23748  kgencmp  23755  kgenidm  23757  iskgen2  23758  kgencn3  23768  ptuni2  23786  ptbasfi  23791  xkouni  23809  txcls  23814  txdis  23842  txindis  23844  txcmplem2  23852  xkopt  23865  txconn  23899  qtopval2  23906  qtopuni  23912  qtoprest  23927  qtopomap  23928  qtopcmap  23929  kqsat  23941  kqcldsat  23943  hmeocls  23978  hmeontr  23979  hmphdis  24006  fgfil  24085  fgabs  24089  trfil1  24096  fgtr  24100  uzrest  24107  ufilmax  24117  ufileu  24129  filufint  24130  ufildom1  24136  rnelfm  24163  flimfil  24179  uffclsflim  24241  alexsublem  24254  alexsubALTlem3  24259  alexsubALT  24261  ptcmplem2  24263  ptcmplem3  24264  tgpconncompeqg  24322  haustsms2  24347  tgptsmscls  24360  ust0  24430  ustbas2  24435  iccntr  25032  pi1xfrcnv  25269  clsocv  25462  cfilfcls  25486  equivcmet  25529  hlhil  25655  evthicc2  25672  ovolshft  25723  volsup  25768  dyadmbllem  25811  mbfconstlem  25839  itg11  25903  limciun  26106  dvnres  26143  cpnord  26147  dvcmulf  26157  dvmptcmul  26176  dvcnvre  26231  plyco0  26402  taylthlem1  26589  taylthlem2  26590  ulmdvlem3  26618  wilthlem2  27286  ppisval  27321  ppinprm  27369  chtnprm  27371  ltsval2  27873  noextenddif  27885  cutsun12  28036  madebdaylemlrcut  28145  bdayiun  28161  cofcut1  28166  negbday  28303  oniso  28517  bdayons  28522  addonbday  28525  bdayn0p1  28615  plngrot  29125  upgrex  29499  uvtxnbgr  29810  cusgredg  29834  ubthlem1  31295  pjhth  31818  ococin  31833  chsupsn  31838  ssjo  31872  chabs1  31941  spansncvi  32077  mdslj1i  32744  mdslj2i  32745  atomli  32807  atcvatlem  32810  atcvat3i  32821  sumdmdlem  32843  difininv  32936  fnpreimac  33088  pmtrcnelor  33477  cycpmrn  33529  elrgspnlem4  33631  fldgenid  33706  1fldgenq  33709  rspidlid  33755  drngmxidl  33825  drngmxidlr  33826  esplyfvaln  34030  resssra  34043  dimkerim  34083  fldextrspunlem1  34131  fldextrspunlem2  34133  algextdeglem4  34176  cmpcref  34306  zarcls1  34325  zarclssn  34329  zart0  34335  zarcmplem  34337  xpinpreima2  34363  ordtrest2NEW  34379  sigagenid  34608  imambfm  34719  reprinfz1  35076  bnj1136  35452  bnj1398  35489  bnj1408  35491  bnj1498  35516  rankval4b  35553  r1omhfb  35568  elscottrankeq  35575  fineqvacALT  35589  r1omhfbregs  35609  vonf1oonfo  35658  sconnpi1  35770  cvmliftlem15  35829  altopthsn  36492  nadddi  36755  opnbnd  36895  opnregcld  36900  cldregopn  36901  fnessref  36927  neibastop1  36929  topmeet  36934  topjoin  36935  fnemeet1  36936  fnejoin1  36938  ttctrid  37072  dfttc2g  37076  dfttc3gw  37093  bj-gabeqd  37632  bj-restpw  37793  bj-restb  37795  bj-restuni2  37799  dissneqlem  38045  pibt2  38122  lindsenlbs  38325  poimirlem13  38343  poimirlem14  38344  poimirlem15  38345  fdc  38456  sstotbnd2  38485  isbnd2  38494  totbndbnd  38500  prdstotbnd  38505  heibor1  38521  1idl  38737  igenval2  38777  idreseqidinxp  39024  disjdmqs  39616  lshpdisj  39821  lssats  39846  lsatcvat3  39886  lshpset2N  39953  lfl1dim  39955  lfl1dim2N  39956  lkrpssN  39997  paddass  40672  paddidm  40675  pmod1i  40682  pmapjat1  40687  pclbtwnN  40731  pclunN  40732  paddunN  40761  pclfinclN  40784  dihjust  42051  dihmeetlem1N  42124  dihglblem5apreN  42125  dihmeetlem13N  42153  dochocsp  42213  dochdmj1  42224  dochnoncon  42225  dihjatb  42250  dihjat1lem  42262  lcfl9a  42339  lclkrlem2s  42359  lclkrlem2v  42362  mapdrvallem3  42480  mapdunirnN  42484  mapdin  42496  mapdlsm  42498  baerlem3lem2  42544  baerlem5alem2  42545  baerlem5blem2  42546  hdmaplkr  42747  primrootsunit1  42924  sticksstones11  42983  aks6d1c6lem5  43004  unitscyglem4  43025  rntrclfvOAI  43482  ismrcd1  43489  ismrcd2  43490  isnacs3  43501  nacsfix  43503  rgspnid  43955  iocinico  43999  onsupmaxb  44026  onsssupeqcond  44067  oacl2g  44117  omabs2  44119  omcl2  44120  ofoaf  44142  onsucunifi  44157  naddwordnexlem4  44188  harval3  44324  mptrcllem  44399  clcnvlem  44409  dmtrcl  44413  rntrcl  44414  cbviuneq12df  44447  dfrcl2  44460  dftrcl3  44506  brtrclfv2  44513  dfrtrcl3  44519  nzin  45088  iunincfi  45872  founiiun  45957  founiiun0  45968  inmap  45985  difmapsn  45988  funimaeq  46021  iuneqfzuz  46111  supminfrnmpt  46219  supminfxr2  46243  supminfxrrnmpt  46245  pimxrneun  46262  iooiinicc  46318  icomnfinre  46328  iooiinioc  46332  limsupresxr  46540  liminfresxr  46541  limsup10exlem  46546  liminfvalxr  46557  fourierdlem79  46959  rrxsnicc  47074  prsal  47092  issalgend  47112  sge0f1o  47156  caragenuni  47285  caragendifcl  47288  opnvonmbllem2  47407  iinhoiicc  47448  pimconstlt1  47476  pimltpnff  47477  pimiooltgt  47484  pimgtmnf2  47488  pimdecfgtioc  47489  pimincfltioc  47490  pimdecfgtioo  47491  pimincfltioo  47492  preimageiingt  47494  preimaleiinlt  47495  pimgtmnff  47496  sssmf  47512  smflimlem5  47549  smfmullem4  47568  smfpimbor1lem2  47573  smfsuplem1  47585  smfpimne2  47614  fsupdm  47616  finfdm  47620  sprsymrelf1  48305  lspeqlco  49278  iunlub  49658  iinglb  49659  iuneqconst2  49660  iineqconst2  49661  isclatd  49820  intubeu  49821  unilbeu  49822  setrecsres  50539