Theorem eqssd 3962

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

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  eqelssd  3966  uneqdifeq  4458  pweq  4581  unieq  4887  unissel  4909  intmin  4937  unissint  4941  int0el  4948  intidg  5439  dmcosseq  5969  dmcosseqOLD  5970  sofld  6186  imadifssran  6203  imadifssranOLD  6204  relfld  6277  preddowncl  6334  frpoind  6344  tz7.7  6387  knatar  7356  sorpssuni  7730  sorpssint  7731  onint  7789  fo2ndf  8116  suppimacnv  8170  tposeq  8224  frrlem14  8296  onfununi  8328  tfrlem15  8379  oaass  8546  odi  8564  omass  8565  oelim2  8581  oeeui  8588  nnawordex  8623  oaabslem  8633  oaabs2  8635  omabslem  8636  omabs  8637  cofon1  8658  uniinqs  8795  sucdom2  9187  onomeneq  9198  fineqv  9227  dffi2  9383  fiuni  9388  dffi3  9391  hartogslem1  9504  ixpiunwdom  9552  cantnfp1lem3  9649  oemapvali  9653  cantnf  9662  dfttrcl2  9693  frind  9722  r1val1  9758  rankval3b  9798  rankunb  9822  rankuni2b  9825  rankr1id  9834  rankc2  9843  rankxplim  9851  tcrank  9856  scottrankd  9874  carden2b  9953  harval2  9983  en2other2  9993  infpwfien  10046  coflim  10245  cfcof  10258  cfidm  10259  isf32lem2  10338  fin1a2lem11  10394  fin1a2lem13  10396  ttukeylem7  10499  fpwwe2  10628  winafp  10682  wuncidm  10731  wuncval2  10732  tskuni  10768  grur1  10805  distrpr  11013  ltexpri  11028  reclem4pr  11035  fzopth  13589  fzosplit  13721  fzouzsplit  13723  fzoopth  13791  ccatrn  14627  cotrtrclfv  15049  dmtrclfv  15055  dfrtrcl2  15099  structcnvcnv  17213  imasaddfnlem  17582  imasvscafn  17591  mrcuni  17677  mressmrcd  17683  submrc  17684  ssceq  17883  rescabs  17890  setcepi  18145  clatl  18564  ipopos  18592  psdmrn  18629  dirdm  18656  gsumress  18740  gsumvallem2  18893  gsumwspan  18905  trivsubgd  19219  trivsubgsnd  19220  trivnsgd  19238  cycsubg  19279  kerf1ghm  19317  conjnmz  19322  pmtrprfv  19523  symggen  19540  odf1o2  19643  gex1  19661  sylow2alem1  19687  smndlsmidm  19726  lsmss1  19735  lsmss2  19737  lsmmod  19745  lsmdisj  19751  lsmdisj2  19752  cntzcmn  19910  prmcyg  19964  dmdprdd  20071  dprdspan  20099  dprdres  20100  dprdz  20102  subgdmdprd  20106  subgdprd  20107  dprddisj2  20111  dprd2dlem1  20113  dprd2da  20114  dmdprdsplit2lem  20117  dprdsplit  20120  ablfacrp  20138  pgpfac1lem3  20149  issubdrg  20861  lspun  21086  lspsn  21101  lspsnneg  21105  lsp0  21108  lsslsp  21114  lmhmlsp  21148  lspextmo  21155  lsmsp  21185  lspprabs  21194  lspsnvs  21216  lspdisj  21227  lsmcv  21243  lspsnat  21247  lsppratlem6  21254  lspprat  21255  lbsextlem4  21263  lidl1el  21329  0ringidl  21338  drngnidl  21351  lidldvgen  21471  cnsubrg  21546  mulgrhm2  21597  znrrg  21684  ocvin  21793  ocvlsp  21795  mrccss  21813  topsn  23057  eltg4i  23086  unitg  23093  tgtop  23099  tgidm  23106  en2top  23111  basgen  23114  2basgen  23116  fctop  23130  cctop  23132  ppttop  23133  epttop  23135  ntrin  23187  isopn3  23192  opnnei  23246  neiuni  23248  maxlp  23273  clslp  23274  tgrest  23285  resttopon  23287  rest0  23295  restcls  23307  restntr  23308  ordtbas2  23317  ordtbas  23318  ordtrest2  23330  cmpcov2  23516  tgcmp  23527  cmpcld  23528  uncmp  23529  cmpfi  23534  dis2ndc  23586  restnlly  23608  dislly  23623  comppfsc  23658  kgentopon  23664  kgencmp  23671  kgenidm  23673  iskgen2  23674  kgencn3  23684  ptuni2  23702  ptbasfi  23707  xkouni  23725  txcls  23730  txdis  23758  txindis  23760  txcmplem2  23768  xkopt  23781  txconn  23815  qtopval2  23822  qtopuni  23828  qtoprest  23843  qtopomap  23844  qtopcmap  23845  kqsat  23857  kqcldsat  23859  hmeocls  23894  hmeontr  23895  hmphdis  23922  fgfil  24001  fgabs  24005  trfil1  24012  fgtr  24016  uzrest  24023  ufilmax  24033  ufileu  24045  filufint  24046  ufildom1  24052  rnelfm  24079  flimfil  24095  uffclsflim  24157  alexsublem  24170  alexsubALTlem3  24175  alexsubALT  24177  ptcmplem2  24179  ptcmplem3  24180  tgpconncompeqg  24238  haustsms2  24263  tgptsmscls  24276  ust0  24346  ustbas2  24351  iccntr  24948  pi1xfrcnv  25185  clsocv  25378  cfilfcls  25402  equivcmet  25445  hlhil  25571  evthicc2  25588  ovolshft  25639  volsup  25684  dyadmbllem  25727  mbfconstlem  25755  itg11  25819  limciun  26022  dvnres  26059  cpnord  26063  dvcmulf  26073  dvmptcmul  26092  dvcnvre  26147  plyco0  26318  taylthlem1  26502  taylthlem2  26503  ulmdvlem3  26531  wilthlem2  27199  ppisval  27234  ppinprm  27282  chtnprm  27284  ltsval2  27786  noextenddif  27798  cutsun12  27949  madebdaylemlrcut  28058  bdayiun  28074  cofcut1  28079  negbday  28216  oniso  28430  bdayons  28435  addonbday  28438  bdayn0p1  28528  plngrot  29030  upgrex  29383  uvtxnbgr  29691  cusgredg  29715  ubthlem1  31163  pjhth  31686  ococin  31701  chsupsn  31706  ssjo  31740  chabs1  31809  spansncvi  31945  mdslj1i  32612  mdslj2i  32613  atomli  32675  atcvatlem  32678  atcvat3i  32689  sumdmdlem  32711  difininv  32804  fnpreimac  32956  pmtrcnelor  33352  cycpmrn  33404  elrgspnlem4  33506  isdrng4  33559  fldgenid  33583  1fldgenq  33586  rspidlid  33632  drngmxidl  33704  drngmxidlr  33705  esplyfvaln  33909  resssra  33922  dimkerim  33962  fldextrspunlem1  34010  fldextrspunlem2  34012  algextdeglem4  34055  cmpcref  34185  zarcls1  34204  zarclssn  34208  zart0  34214  zarcmplem  34216  xpinpreima2  34242  ordtrest2NEW  34258  sigagenid  34486  imambfm  34597  reprinfz1  34954  bnj1136  35330  bnj1398  35367  bnj1408  35369  bnj1498  35394  rankval4b  35436  r1omhfb  35448  fineqvacALT  35453  r1omhfbregs  35473  vonf1oonfo  35498  sconnpi1  35630  cvmliftlem15  35689  altopthsn  36352  opnbnd  36725  opnregcld  36730  cldregopn  36731  fnessref  36757  neibastop1  36759  topmeet  36764  topjoin  36765  fnemeet1  36766  fnejoin1  36768  ttctrid  36902  dfttc2g  36906  dfttc3gw  36923  bj-gabeqd  37461  bj-restpw  37622  bj-restb  37624  bj-restuni2  37628  dissneqlem  37874  pibt2  37951  lindsenlbs  38154  poimirlem13  38172  poimirlem14  38173  poimirlem15  38174  fdc  38284  sstotbnd2  38313  isbnd2  38322  totbndbnd  38328  prdstotbnd  38333  heibor1  38349  1idl  38565  igenval2  38605  idreseqidinxp  38854  disjdmqs  39446  lshpdisj  39651  lssats  39676  lsatcvat3  39716  lshpset2N  39783  lfl1dim  39785  lfl1dim2N  39786  lkrpssN  39827  paddass  40502  paddidm  40505  pmod1i  40512  pmapjat1  40517  pclbtwnN  40561  pclunN  40562  paddunN  40591  pclfinclN  40614  dihjust  41881  dihmeetlem1N  41954  dihglblem5apreN  41955  dihmeetlem13N  41983  dochocsp  42043  dochdmj1  42054  dochnoncon  42055  dihjatb  42080  dihjat1lem  42092  lcfl9a  42169  lclkrlem2s  42189  lclkrlem2v  42192  mapdrvallem3  42310  mapdunirnN  42314  mapdin  42326  mapdlsm  42328  baerlem3lem2  42374  baerlem5alem2  42375  baerlem5blem2  42376  hdmaplkr  42577  primrootsunit1  42754  sticksstones11  42813  aks6d1c6lem5  42834  unitscyglem4  42855  rntrclfvOAI  43314  ismrcd1  43321  ismrcd2  43322  isnacs3  43333  nacsfix  43335  rgspnid  43787  iocinico  43831  onsupmaxb  43858  onsssupeqcond  43899  oacl2g  43949  omabs2  43951  omcl2  43952  ofoaf  43974  onsucunifi  43989  naddwordnexlem4  44020  harval3  44156  mptrcllem  44231  clcnvlem  44241  dmtrcl  44245  rntrcl  44246  cbviuneq12df  44279  dfrcl2  44292  dftrcl3  44338  brtrclfv2  44345  dfrtrcl3  44351  nzin  44920  iunincfi  45704  founiiun  45789  founiiun0  45800  inmap  45817  difmapsn  45820  funimaeq  45853  iuneqfzuz  45943  supminfrnmpt  46051  supminfxr2  46075  supminfxrrnmpt  46077  pimxrneun  46094  iooiinicc  46150  icomnfinre  46160  iooiinioc  46164  limsupresxr  46372  liminfresxr  46373  limsup10exlem  46378  liminfvalxr  46389  fourierdlem79  46791  rrxsnicc  46906  prsal  46924  issalgend  46944  sge0f1o  46988  caragenuni  47117  caragendifcl  47120  opnvonmbllem2  47239  iinhoiicc  47280  pimconstlt1  47308  pimltpnff  47309  pimiooltgt  47316  pimgtmnf2  47320  pimdecfgtioc  47321  pimincfltioc  47322  pimdecfgtioo  47323  pimincfltioo  47324  preimageiingt  47326  preimaleiinlt  47327  pimgtmnff  47328  sssmf  47344  smflimlem5  47381  smfmullem4  47400  smfpimbor1lem2  47405  smfsuplem1  47417  smfpimne2  47446  fsupdm  47448  finfdm  47452  sprsymrelf1  48134  lspeqlco  49104  iunlub  49484  iinglb  49485  iuneqconst2  49486  iineqconst2  49487  isclatd  49646  intubeu  49647  unilbeu  49648  setrecsres  50365