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 584	1 ⊢ (𝜑 → 𝐴 = 𝐵)

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3889

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  eqelssd  3943  uneqdifeq  4432  pweq  4555  unieq  4861  unissel  4882  intmin  4910  unissint  4914  int0el  4921  intidg  5409  dmcosseq  5933  dmcosseqOLD  5934  dmcosseqOLDOLD  5935  imadifssran  6115  sofld  6151  relfld  6239  preddowncl  6296  frpoind  6306  tz7.7  6349  f1imadifssran  6584  knatar  7312  sorpssuni  7686  sorpssint  7687  onint  7744  fo2ndf  8071  suppimacnv  8124  tposeq  8178  frrlem14  8249  onfununi  8281  tfrlem15  8331  oaass  8496  odi  8514  omass  8515  oelim2  8531  oeeui  8538  nnawordex  8573  oaabslem  8583  oaabs2  8585  omabslem  8586  omabs  8587  cofon1  8608  uniinqs  8744  sucdom2  9137  onomeneq  9148  fineqv  9177  dffi2  9336  fiuni  9341  dffi3  9344  hartogslem1  9457  ixpiunwdom  9505  cantnfp1lem3  9601  oemapvali  9605  cantnf  9614  dfttrcl2  9645  frind  9674  r1val1  9710  rankval3b  9750  rankunb  9774  rankuni2b  9777  rankr1id  9786  rankc2  9795  rankxplim  9803  tcrank  9808  carden2b  9891  harval2  9921  en2other2  9931  infpwfien  9984  coflim  10183  cfcof  10196  cfidm  10197  isf32lem2  10276  fin1a2lem11  10332  fin1a2lem13  10334  ttukeylem7  10437  fpwwe2  10566  winafp  10620  wuncidm  10669  wuncval2  10670  tskuni  10706  grur1  10743  distrpr  10951  ltexpri  10966  reclem4pr  10973  fzopth  13515  fzosplit  13647  fzouzsplit  13649  fzoopth  13717  ccatrn  14552  cotrtrclfv  14974  dmtrclfv  14980  dfrtrcl2  15024  structcnvcnv  17123  imasaddfnlem  17492  imasvscafn  17501  mrcuni  17587  mressmrcd  17593  submrc  17594  ssceq  17793  rescabs  17800  setcepi  18055  clatl  18474  ipopos  18502  psdmrn  18539  dirdm  18566  gsumress  18650  gsumvallem2  18802  gsumwspan  18814  trivsubgd  19128  trivsubgsnd  19129  trivnsgd  19147  cycsubg  19183  kerf1ghm  19222  conjnmz  19227  pmtrprfv  19428  symggen  19445  odf1o2  19548  gex1  19566  sylow2alem1  19592  smndlsmidm  19631  lsmss1  19640  lsmss2  19642  lsmmod  19650  lsmdisj  19656  lsmdisj2  19657  cntzcmn  19815  prmcyg  19869  dmdprdd  19976  dprdspan  20004  dprdres  20005  dprdz  20007  subgdmdprd  20011  subgdprd  20012  dprddisj2  20016  dprd2dlem1  20018  dprd2da  20019  dmdprdsplit2lem  20022  dprdsplit  20025  ablfacrp  20043  pgpfac1lem3  20054  issubdrg  20757  lspun  20982  lspsn  20997  lspsnneg  21001  lsp0  21004  lsslsp  21010  lmhmlsp  21044  lspextmo  21051  lsmsp  21081  lspprabs  21090  lspsnvs  21112  lspdisj  21123  lsmcv  21139  lspsnat  21143  lsppratlem6  21150  lspprat  21151  lbsextlem4  21159  lidl1el  21224  drngnidl  21241  lidldvgen  21332  cnsubrg  21407  mulgrhm2  21458  znrrg  21545  ocvin  21654  ocvlsp  21656  mrccss  21674  topsn  22896  eltg4i  22925  unitg  22932  tgtop  22938  tgidm  22945  en2top  22950  basgen  22953  2basgen  22955  fctop  22969  cctop  22971  ppttop  22972  epttop  22974  ntrin  23026  isopn3  23031  opnnei  23085  neiuni  23087  maxlp  23112  clslp  23113  tgrest  23124  resttopon  23126  rest0  23134  restcls  23146  restntr  23147  ordtbas2  23156  ordtbas  23157  ordtrest2  23169  cmpcov2  23355  tgcmp  23366  cmpcld  23367  uncmp  23368  cmpfi  23373  dis2ndc  23425  restnlly  23447  dislly  23462  comppfsc  23497  kgentopon  23503  kgencmp  23510  kgenidm  23512  iskgen2  23513  kgencn3  23523  ptuni2  23541  ptbasfi  23546  xkouni  23564  txcls  23569  txdis  23597  txindis  23599  txcmplem2  23607  xkopt  23620  txconn  23654  qtopval2  23661  qtopuni  23667  qtoprest  23682  qtopomap  23683  qtopcmap  23684  kqsat  23696  kqcldsat  23698  hmeocls  23733  hmeontr  23734  hmphdis  23761  fgfil  23840  fgabs  23844  trfil1  23851  fgtr  23855  uzrest  23862  ufilmax  23872  ufileu  23884  filufint  23885  ufildom1  23891  rnelfm  23918  flimfil  23934  uffclsflim  23996  alexsublem  24009  alexsubALTlem3  24014  alexsubALT  24016  ptcmplem2  24018  ptcmplem3  24019  tgpconncompeqg  24077  haustsms2  24102  tgptsmscls  24115  ust0  24185  ustbas2  24190  iccntr  24787  pi1xfrcnv  25024  clsocv  25217  cfilfcls  25241  equivcmet  25284  hlhil  25410  evthicc2  25427  ovolshft  25478  volsup  25523  dyadmbllem  25566  mbfconstlem  25594  itg11  25658  limciun  25861  dvnres  25898  cpnord  25902  dvcmulf  25912  dvmptcmul  25931  dvcnvre  25986  plyco0  26157  taylthlem1  26338  taylthlem2  26339  ulmdvlem3  26367  wilthlem2  27032  ppisval  27067  ppinprm  27115  chtnprm  27117  ltsval2  27620  noextenddif  27632  cutsun12  27782  madebdaylemlrcut  27891  bdayiun  27907  cofcut1  27912  negbday  28049  oniso  28263  bdayons  28268  addonbday  28271  bdayn0p1  28361  upgrex  29161  uvtxnbgr  29469  cusgredg  29493  ubthlem1  30941  pjhth  31464  ococin  31479  chsupsn  31484  ssjo  31518  chabs1  31587  spansncvi  31723  mdslj1i  32390  mdslj2i  32391  atomli  32453  atcvatlem  32456  atcvat3i  32467  sumdmdlem  32489  difininv  32587  fnpreimac  32743  pmtrcnelor  33152  cycpmrn  33204  elrgspnlem4  33306  isdrng4  33356  fldgenid  33380  1fldgenq  33383  rspidlid  33435  0ringidl  33481  drngmxidl  33537  drngmxidlr  33538  esplyfvaln  33718  resssra  33731  dimkerim  33771  fldextrspunlem1  33819  fldextrspunlem2  33821  algextdeglem4  33864  cmpcref  33994  zarcls1  34013  zarclssn  34017  zart0  34023  zarcmplem  34025  xpinpreima2  34051  ordtrest2NEW  34067  sigagenid  34295  imambfm  34406  reprinfz1  34766  bnj1136  35139  bnj1398  35176  bnj1408  35178  bnj1498  35203  rankval4b  35243  r1omhfb  35256  fineqvacALT  35261  r1omhfbregs  35281  sconnpi1  35421  cvmliftlem15  35480  altopthsn  36143  opnbnd  36507  opnregcld  36512  cldregopn  36513  fnessref  36539  neibastop1  36541  topmeet  36546  topjoin  36547  fnemeet1  36548  fnejoin1  36550  ttctrid  36684  dfttc2g  36688  dfttc3gw  36705  bj-gabeqd  37244  bj-restpw  37404  bj-restb  37406  bj-restuni2  37410  dissneqlem  37656  pibt2  37733  lindsenlbs  37936  poimirlem13  37954  poimirlem14  37955  poimirlem15  37956  fdc  38066  sstotbnd2  38095  isbnd2  38104  totbndbnd  38110  prdstotbnd  38115  heibor1  38131  1idl  38347  igenval2  38387  idreseqidinxp  38636  disjdmqs  39228  lshpdisj  39433  lssats  39458  lsatcvat3  39498  lshpset2N  39565  lfl1dim  39567  lfl1dim2N  39568  lkrpssN  39609  paddass  40284  paddidm  40287  pmod1i  40294  pmapjat1  40299  pclbtwnN  40343  pclunN  40344  paddunN  40373  pclfinclN  40396  dihjust  41663  dihmeetlem1N  41736  dihglblem5apreN  41737  dihmeetlem13N  41765  dochocsp  41825  dochdmj1  41836  dochnoncon  41837  dihjatb  41862  dihjat1lem  41874  lcfl9a  41951  lclkrlem2s  41971  lclkrlem2v  41974  mapdrvallem3  42092  mapdunirnN  42096  mapdin  42108  mapdlsm  42110  baerlem3lem2  42156  baerlem5alem2  42157  baerlem5blem2  42158  hdmaplkr  42359  primrootsunit1  42536  sticksstones11  42595  aks6d1c6lem5  42616  unitscyglem4  42637  rntrclfvOAI  43123  ismrcd1  43130  ismrcd2  43131  isnacs3  43142  nacsfix  43144  rgspnid  43596  iocinico  43640  onsupmaxb  43667  onsssupeqcond  43708  oacl2g  43758  omabs2  43760  omcl2  43761  ofoaf  43783  onsucunifi  43798  naddwordnexlem4  43829  harval3  43965  mptrcllem  44040  clcnvlem  44050  dmtrcl  44054  rntrcl  44055  cbviuneq12df  44088  dfrcl2  44101  dftrcl3  44147  brtrclfv2  44154  dfrtrcl3  44160  scottrankd  44675  nzin  44745  iunincfi  45524  founiiun  45609  founiiun0  45620  inmap  45638  difmapsn  45641  funimaeq  45675  iuneqfzuz  45765  supminfrnmpt  45873  supminfxr2  45897  supminfxrrnmpt  45899  pimxrneun  45916  iooiinicc  45972  icomnfinre  45982  iooiinioc  45986  limsupresxr  46194  liminfresxr  46195  limsup10exlem  46200  liminfvalxr  46211  fourierdlem79  46613  rrxsnicc  46728  prsal  46746  issalgend  46766  sge0f1o  46810  caragenuni  46939  caragendifcl  46942  opnvonmbllem2  47061  iinhoiicc  47102  pimconstlt1  47130  pimltpnff  47131  pimiooltgt  47138  pimgtmnf2  47142  pimdecfgtioc  47143  pimincfltioc  47144  pimdecfgtioo  47145  pimincfltioo  47146  preimageiingt  47148  preimaleiinlt  47149  pimgtmnff  47150  sssmf  47166  smflimlem5  47203  smfmullem4  47222  smfpimbor1lem2  47227  smfsuplem1  47239  smfpimne2  47268  fsupdm  47270  finfdm  47274  sprsymrelf1  47956  lspeqlco  48915  iunlub  49296  iinglb  49297  iuneqconst2  49298  iineqconst2  49299  isclatd  49458  intubeu  49459  unilbeu  49460  setrecsres  50177