Theorem eqssd 3954

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3922

This theorem is referenced by:  eqelssd  3958  uneqdifeq  4453  pweq  4576  unieq  4883  unissel  4905  intmin  4933  unissint  4937  int0el  4944  intidg  5438  dmcosseq  5968  dmcosseqOLD  5969  sofld  6185  imadifssran  6202  imadifssranOLD  6203  relfld  6276  preddowncl  6333  frpoind  6343  tz7.7  6386  knatar  7355  sorpssuni  7729  sorpssint  7730  onint  7785  fo2ndf  8112  suppimacnv  8166  tposeq  8220  frrlem14  8292  onfununi  8324  tfrlem15  8375  oaass  8542  odi  8560  omass  8561  oelim2  8577  oeeui  8584  nnawordex  8619  oaabslem  8629  oaabs2  8631  omabslem  8632  omabs  8633  cofon1  8654  uniinqs  8791  sucdom2  9183  onomeneq  9194  fineqv  9223  dffi2  9379  fiuni  9384  dffi3  9387  hartogslem1  9500  ixpiunwdom  9548  cantnfp1lem3  9645  oemapvali  9649  cantnf  9658  dfttrcl2  9689  frind  9718  r1val1  9754  rankval3b  9794  rankunb  9818  rankuni2b  9821  rankr1id  9830  rankc2  9839  rankxplim  9847  tcrank  9852  scottrankd  9870  carden2b  9949  harval2  9979  en2other2  9989  infpwfien  10042  coflim  10240  cfcof  10253  cfidm  10254  isf32lem2  10333  fin1a2lem11  10389  fin1a2lem13  10391  ttukeylem7  10494  fpwwe2  10623  winafp  10677  wuncidm  10726  wuncval2  10727  tskuni  10763  grur1  10800  distrpr  11008  ltexpri  11023  reclem4pr  11030  fzopth  13585  fzosplit  13717  fzouzsplit  13719  fzoopth  13787  ccatrn  14623  cotrtrclfv  15045  dmtrclfv  15051  dfrtrcl2  15095  structcnvcnv  17208  imasaddfnlem  17577  imasvscafn  17586  mrcuni  17672  mressmrcd  17678  submrc  17679  ssceq  17878  rescabs  17885  setcepi  18140  clatl  18559  ipopos  18587  psdmrn  18624  dirdm  18651  gsumress  18735  gsumvallem2  18888  gsumwspan  18900  trivsubgd  19214  trivsubgsnd  19215  trivnsgd  19233  cycsubg  19274  kerf1ghm  19312  conjnmz  19317  pmtrprfv  19518  symggen  19535  odf1o2  19638  gex1  19656  sylow2alem1  19682  smndlsmidm  19721  lsmss1  19730  lsmss2  19732  lsmmod  19740  lsmdisj  19746  lsmdisj2  19747  cntzcmn  19905  prmcyg  19959  dmdprdd  20066  dprdspan  20094  dprdres  20095  dprdz  20097  subgdmdprd  20101  subgdprd  20102  dprddisj2  20106  dprd2dlem1  20108  dprd2da  20109  dmdprdsplit2lem  20112  dprdsplit  20115  ablfacrp  20133  pgpfac1lem3  20144  isdrng4  20839  issubdrg  20883  lspun  21108  lspsn  21123  lspsnneg  21127  lsp0  21130  lsslsp  21136  lmhmlsp  21170  lspextmo  21177  lsmsp  21207  lspprabs  21216  lspsnvs  21238  lspdisj  21249  lsmcv  21265  lspsnat  21269  lsppratlem6  21276  lspprat  21277  lbsextlem4  21285  lidl1el  21351  0ringidl  21360  rspprop  21370  drngnidl  21377  lidldvgen  21502  cnsubrg  21577  mulgrhm2  21628  znrrg  21715  ocvin  21824  ocvlsp  21826  mrccss  21844  topsn  23088  eltg4i  23117  unitg  23124  tgtop  23130  tgidm  23137  en2top  23142  basgen  23145  2basgen  23147  fctop  23161  cctop  23163  ppttop  23164  epttop  23166  ntrin  23218  isopn3  23223  opnnei  23277  neiuni  23279  maxlp  23304  clslp  23305  tgrest  23316  resttopon  23318  rest0  23326  restcls  23338  restntr  23339  ordtbas2  23348  ordtbas  23349  ordtrest2  23361  cmpcov2  23547  tgcmp  23558  cmpcld  23559  uncmp  23560  cmpfi  23565  dis2ndc  23617  restnlly  23639  dislly  23654  comppfsc  23689  kgentopon  23695  kgencmp  23702  kgenidm  23704  iskgen2  23705  kgencn3  23715  ptuni2  23733  ptbasfi  23738  xkouni  23756  txcls  23761  txdis  23789  txindis  23791  txcmplem2  23799  xkopt  23812  txconn  23846  qtopval2  23853  qtopuni  23859  qtoprest  23874  qtopomap  23875  qtopcmap  23876  kqsat  23888  kqcldsat  23890  hmeocls  23925  hmeontr  23926  hmphdis  23953  fgfil  24032  fgabs  24036  trfil1  24043  fgtr  24047  uzrest  24054  ufilmax  24064  ufileu  24076  filufint  24077  ufildom1  24083  rnelfm  24110  flimfil  24126  uffclsflim  24188  alexsublem  24201  alexsubALTlem3  24206  alexsubALT  24208  ptcmplem2  24210  ptcmplem3  24211  tgpconncompeqg  24269  haustsms2  24294  tgptsmscls  24307  ust0  24377  ustbas2  24382  iccntr  24979  pi1xfrcnv  25216  clsocv  25409  cfilfcls  25433  equivcmet  25476  hlhil  25602  evthicc2  25619  ovolshft  25670  volsup  25715  dyadmbllem  25758  mbfconstlem  25786  itg11  25850  limciun  26053  dvnres  26090  cpnord  26094  dvcmulf  26104  dvmptcmul  26123  dvcnvre  26178  plyco0  26349  taylthlem1  26536  taylthlem2  26537  ulmdvlem3  26565  wilthlem2  27233  ppisval  27268  ppinprm  27316  chtnprm  27318  ltsval2  27820  noextenddif  27832  cutsun12  27983  madebdaylemlrcut  28092  bdayiun  28108  cofcut1  28113  negbday  28250  oniso  28464  bdayons  28469  addonbday  28472  bdayn0p1  28562  plngrot  29072  upgrex  29442  uvtxnbgr  29750  cusgredg  29774  ubthlem1  31222  pjhth  31745  ococin  31760  chsupsn  31765  ssjo  31799  chabs1  31868  spansncvi  32004  mdslj1i  32671  mdslj2i  32672  atomli  32734  atcvatlem  32737  atcvat3i  32748  sumdmdlem  32770  difininv  32863  fnpreimac  33015  pmtrcnelor  33411  cycpmrn  33463  elrgspnlem4  33565  fldgenid  33640  1fldgenq  33643  rspidlid  33689  drngmxidl  33759  drngmxidlr  33760  esplyfvaln  33964  resssra  33977  dimkerim  34017  fldextrspunlem1  34065  fldextrspunlem2  34067  algextdeglem4  34110  cmpcref  34240  zarcls1  34259  zarclssn  34263  zart0  34269  zarcmplem  34271  xpinpreima2  34297  ordtrest2NEW  34313  sigagenid  34541  imambfm  34652  reprinfz1  35009  bnj1136  35385  bnj1398  35422  bnj1408  35424  bnj1498  35449  rankval4b  35493  r1omhfb  35508  elscottrankeq  35515  fineqvacALT  35530  r1omhfbregs  35550  vonf1oonfo  35599  sconnpi1  35731  cvmliftlem15  35790  altopthsn  36453  nadddi  36716  opnbnd  36856  opnregcld  36861  cldregopn  36862  fnessref  36888  neibastop1  36890  topmeet  36895  topjoin  36896  fnemeet1  36897  fnejoin1  36899  ttctrid  37033  dfttc2g  37037  dfttc3gw  37054  bj-gabeqd  37593  bj-restpw  37754  bj-restb  37756  bj-restuni2  37760  dissneqlem  38006  pibt2  38083  lindsenlbs  38286  poimirlem13  38304  poimirlem14  38305  poimirlem15  38306  fdc  38416  sstotbnd2  38445  isbnd2  38454  totbndbnd  38460  prdstotbnd  38465  heibor1  38481  1idl  38697  igenval2  38737  idreseqidinxp  38984  disjdmqs  39576  lshpdisj  39781  lssats  39806  lsatcvat3  39846  lshpset2N  39913  lfl1dim  39915  lfl1dim2N  39916  lkrpssN  39957  paddass  40632  paddidm  40635  pmod1i  40642  pmapjat1  40647  pclbtwnN  40691  pclunN  40692  paddunN  40721  pclfinclN  40744  dihjust  42011  dihmeetlem1N  42084  dihglblem5apreN  42085  dihmeetlem13N  42113  dochocsp  42173  dochdmj1  42184  dochnoncon  42185  dihjatb  42210  dihjat1lem  42222  lcfl9a  42299  lclkrlem2s  42319  lclkrlem2v  42322  mapdrvallem3  42440  mapdunirnN  42444  mapdin  42456  mapdlsm  42458  baerlem3lem2  42504  baerlem5alem2  42505  baerlem5blem2  42506  hdmaplkr  42707  primrootsunit1  42884  sticksstones11  42943  aks6d1c6lem5  42964  unitscyglem4  42985  rntrclfvOAI  43442  ismrcd1  43449  ismrcd2  43450  isnacs3  43461  nacsfix  43463  rgspnid  43915  iocinico  43959  onsupmaxb  43986  onsssupeqcond  44027  oacl2g  44077  omabs2  44079  omcl2  44080  ofoaf  44102  onsucunifi  44117  naddwordnexlem4  44148  harval3  44284  mptrcllem  44359  clcnvlem  44369  dmtrcl  44373  rntrcl  44374  cbviuneq12df  44407  dfrcl2  44420  dftrcl3  44466  brtrclfv2  44473  dfrtrcl3  44479  nzin  45048  iunincfi  45832  founiiun  45917  founiiun0  45928  inmap  45945  difmapsn  45948  funimaeq  45981  iuneqfzuz  46071  supminfrnmpt  46179  supminfxr2  46203  supminfxrrnmpt  46205  pimxrneun  46222  iooiinicc  46278  icomnfinre  46288  iooiinioc  46292  limsupresxr  46500  liminfresxr  46501  limsup10exlem  46506  liminfvalxr  46517  fourierdlem79  46919  rrxsnicc  47034  prsal  47052  issalgend  47072  sge0f1o  47116  caragenuni  47245  caragendifcl  47248  opnvonmbllem2  47367  iinhoiicc  47408  pimconstlt1  47436  pimltpnff  47437  pimiooltgt  47444  pimgtmnf2  47448  pimdecfgtioc  47449  pimincfltioc  47450  pimdecfgtioo  47451  pimincfltioo  47452  preimageiingt  47454  preimaleiinlt  47455  pimgtmnff  47456  sssmf  47472  smflimlem5  47509  smfmullem4  47528  smfpimbor1lem2  47533  smfsuplem1  47545  smfpimne2  47574  fsupdm  47576  finfdm  47580  sprsymrelf1  48265  lspeqlco  49239  iunlub  49619  iinglb  49620  iuneqconst2  49621  iineqconst2  49622  isclatd  49781  intubeu  49782  unilbeu  49783  setrecsres  50500