Theorem eqssd 4012

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

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  eqelssd  4016  uneqdifeq  4498  pweq  4618  unieq  4922  unissel  4942  intmin  4972  unissint  4976  int0el  4983  intidg  5467  dmcosseq  5989  dmcosseqOLD  5990  sofld  6208  relfld  6296  preddowncl  6354  frpoind  6364  wfiOLD  6373  tz7.7  6411  knatar  7376  sorpssuni  7750  sorpssint  7751  onint  7809  fo2ndf  8144  suppimacnv  8197  tposeq  8251  frrlem14  8322  onfununi  8379  tfrlem15  8430  oaass  8597  odi  8615  omass  8616  oelim2  8631  oeeui  8638  nnawordex  8673  oaabslem  8683  oaabs2  8685  omabslem  8686  omabs  8687  cofon1  8708  uniinqs  8835  sucdom2OLD  9120  sucdom2  9240  onomeneq  9262  fineqv  9296  dffi2  9460  fiuni  9465  dffi3  9468  hartogslem1  9579  ixpiunwdom  9627  cantnfp1lem3  9717  oemapvali  9721  cantnf  9730  dfttrcl2  9761  frind  9787  r1val1  9823  rankval3b  9863  rankunb  9887  rankuni2b  9890  rankr1id  9899  rankc2  9908  rankxplim  9916  tcrank  9921  carden2b  10004  harval2  10034  en2other2  10046  infpwfien  10099  coflim  10298  cfcof  10311  cfidm  10312  isf32lem2  10391  fin1a2lem11  10447  fin1a2lem13  10449  ttukeylem7  10552  fpwwe2  10680  winafp  10734  wuncidm  10783  wuncval2  10784  tskuni  10820  grur1  10857  distrpr  11065  ltexpri  11080  reclem4pr  11087  fzopth  13597  fzosplit  13728  fzouzsplit  13730  fzoopth  13797  ccatrn  14623  cotrtrclfv  15047  dmtrclfv  15053  dfrtrcl2  15097  structcnvcnv  17186  imasaddfnlem  17574  imasvscafn  17583  mrcuni  17665  mressmrcd  17671  submrc  17672  ssceq  17873  rescabs  17882  rescabsOLD  17883  setcepi  18141  clatl  18565  ipopos  18593  psdmrn  18630  dirdm  18657  gsumress  18707  gsumvallem2  18859  gsumwspan  18871  trivsubgd  19183  trivsubgsnd  19184  trivnsgd  19202  cycsubg  19238  kerf1ghm  19277  conjnmz  19282  pmtrprfv  19485  symggen  19502  odf1o2  19605  gex1  19623  sylow2alem1  19649  smndlsmidm  19688  lsmss1  19697  lsmss2  19699  lsmmod  19707  lsmdisj  19713  lsmdisj2  19714  cntzcmn  19872  prmcyg  19926  dmdprdd  20033  dprdspan  20061  dprdres  20062  dprdz  20064  subgdmdprd  20068  subgdprd  20069  dprddisj2  20073  dprd2dlem1  20075  dprd2da  20076  dmdprdsplit2lem  20079  dprdsplit  20082  ablfacrp  20100  pgpfac1lem3  20111  issubdrg  20797  lspun  21002  lspsn  21017  lspsnneg  21021  lsp0  21024  lsslsp  21030  lsslspOLD  21031  lmhmlsp  21065  lspextmo  21072  lsmsp  21102  lspprabs  21111  lspsnvs  21133  lspdisj  21144  lsmcv  21160  lspsnat  21164  lsppratlem6  21171  lspprat  21172  lbsextlem4  21180  lidl1el  21253  drngnidl  21270  lidldvgen  21361  cnsubrg  21462  mulgrhm2  21506  znrrg  21601  ocvin  21709  ocvlsp  21711  mrccss  21729  topsn  22952  eltg4i  22982  unitg  22989  tgtop  22995  tgidm  23002  en2top  23007  basgen  23010  2basgen  23012  fctop  23026  cctop  23028  ppttop  23029  epttop  23031  ntrin  23084  isopn3  23089  opnnei  23143  neiuni  23145  maxlp  23170  clslp  23171  tgrest  23182  resttopon  23184  rest0  23192  restcls  23204  restntr  23205  ordtbas2  23214  ordtbas  23215  ordtrest2  23227  cmpcov2  23413  tgcmp  23424  cmpcld  23425  uncmp  23426  cmpfi  23431  dis2ndc  23483  restnlly  23505  dislly  23520  comppfsc  23555  kgentopon  23561  kgencmp  23568  kgenidm  23570  iskgen2  23571  kgencn3  23581  ptuni2  23599  ptbasfi  23604  xkouni  23622  txcls  23627  txdis  23655  txindis  23657  txcmplem2  23665  xkopt  23678  txconn  23712  qtopval2  23719  qtopuni  23725  qtoprest  23740  qtopomap  23741  qtopcmap  23742  kqsat  23754  kqcldsat  23756  hmeocls  23791  hmeontr  23792  hmphdis  23819  fgfil  23898  fgabs  23902  trfil1  23909  fgtr  23913  uzrest  23920  ufilmax  23930  ufileu  23942  filufint  23943  ufildom1  23949  rnelfm  23976  flimfil  23992  uffclsflim  24054  alexsublem  24067  alexsubALTlem3  24072  alexsubALT  24074  ptcmplem2  24076  ptcmplem3  24077  tgpconncompeqg  24135  haustsms2  24160  tgptsmscls  24173  ust0  24243  ustbas2  24249  iccntr  24856  pi1xfrcnv  25103  clsocv  25297  cfilfcls  25321  equivcmet  25364  hlhil  25490  evthicc2  25508  ovolshft  25559  volsup  25604  dyadmbllem  25647  mbfconstlem  25675  itg11  25739  limciun  25943  dvnres  25981  cpnord  25985  dvcmulf  25996  dvmptcmul  26016  dvcnvre  26072  plyco0  26245  taylthlem1  26429  taylthlem2  26430  taylthlem2OLD  26431  ulmdvlem3  26459  wilthlem2  27126  ppisval  27161  ppinprm  27209  chtnprm  27211  sltval2  27715  noextenddif  27727  scutun12  27869  madebdaylemlrcut  27951  cofcut1  27968  negsbday  28103  upgrex  29123  uvtxnbgr  29431  cusgredg  29455  ubthlem1  30898  pjhth  31421  ococin  31436  chsupsn  31441  ssjo  31475  chabs1  31544  spansncvi  31680  mdslj1i  32347  mdslj2i  32348  atomli  32410  atcvatlem  32413  atcvat3i  32424  sumdmdlem  32446  difininv  32544  fnpreimac  32687  pmtrcnelor  33093  cycpmrn  33145  elrgspnlem4  33234  isdrng4  33278  fldgenid  33300  1fldgenq  33303  rspidlid  33382  0ringidl  33428  drngmxidl  33484  drngmxidlr  33485  resssra  33616  dimkerim  33654  algextdeglem4  33725  cmpcref  33810  zarcls1  33829  zarclssn  33833  zart0  33839  zarcmplem  33841  xpinpreima2  33867  ordtrest2NEW  33883  sigagenid  34131  imambfm  34243  reprinfz1  34615  bnj1136  34989  bnj1398  35026  bnj1408  35028  bnj1498  35053  fineqvacALT  35090  sconnpi1  35223  cvmliftlem15  35282  altopthsn  35942  opnbnd  36307  opnregcld  36312  cldregopn  36313  fnessref  36339  neibastop1  36341  topmeet  36346  topjoin  36347  fnemeet1  36348  fnejoin1  36350  bj-gabeqd  36919  bj-restpw  37074  bj-restb  37076  bj-restuni2  37080  dissneqlem  37322  pibt2  37399  lindsenlbs  37601  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  fdc  37731  sstotbnd2  37760  isbnd2  37769  totbndbnd  37775  prdstotbnd  37780  heibor1  37796  1idl  38012  igenval2  38052  idreseqidinxp  38290  disjdmqs  38785  lshpdisj  38968  lssats  38993  lsatcvat3  39033  lshpset2N  39100  lfl1dim  39102  lfl1dim2N  39103  lkrpssN  39144  paddass  39820  paddidm  39823  pmod1i  39830  pmapjat1  39835  pclbtwnN  39879  pclunN  39880  paddunN  39909  pclfinclN  39932  dihjust  41199  dihmeetlem1N  41272  dihglblem5apreN  41273  dihmeetlem13N  41301  dochocsp  41361  dochdmj1  41372  dochnoncon  41373  dihjatb  41398  dihjat1lem  41410  lcfl9a  41487  lclkrlem2s  41507  lclkrlem2v  41510  mapdrvallem3  41628  mapdunirnN  41632  mapdin  41644  mapdlsm  41646  baerlem3lem2  41692  baerlem5alem2  41693  baerlem5blem2  41694  hdmaplkr  41895  primrootsunit1  42078  sticksstones11  42137  aks6d1c6lem5  42158  unitscyglem4  42179  rntrclfvOAI  42678  ismrcd1  42685  ismrcd2  42686  isnacs3  42697  nacsfix  42699  rgspnid  43156  iocinico  43200  onsupmaxb  43227  onsssupeqcond  43269  oacl2g  43319  omabs2  43321  omcl2  43322  ofoaf  43344  onsucunifi  43359  naddwordnexlem4  43390  harval3  43527  mptrcllem  43602  clcnvlem  43612  dmtrcl  43616  rntrcl  43617  cbviuneq12df  43650  dfrcl2  43663  dftrcl3  43709  brtrclfv2  43716  dfrtrcl3  43722  scottrankd  44243  nzin  44313  iunincfi  45033  founiiun  45121  founiiun0  45132  inmap  45151  difmapsn  45154  funimaeq  45190  iuneqfzuz  45284  supminfrnmpt  45394  supminfxr2  45418  supminfxrrnmpt  45420  pimxrneun  45438  iooiinicc  45494  icomnfinre  45504  iooiinioc  45508  limsupresxr  45721  liminfresxr  45722  limsup10exlem  45727  liminfvalxr  45738  fourierdlem79  46140  rrxsnicc  46255  prsal  46273  issalgend  46293  sge0f1o  46337  caragenuni  46466  caragendifcl  46469  opnvonmbllem2  46588  iinhoiicc  46629  pimconstlt1  46657  pimltpnff  46658  pimiooltgt  46665  pimgtmnf2  46669  pimdecfgtioc  46670  pimincfltioc  46671  pimdecfgtioo  46672  pimincfltioo  46673  preimageiingt  46675  preimaleiinlt  46676  pimgtmnff  46677  sssmf  46693  smflimlem5  46730  smfmullem4  46749  smfpimbor1lem2  46754  smfsuplem1  46766  smfpimne2  46795  fsupdm  46797  finfdm  46801  sprsymrelf1  47420  lspeqlco  48284  isclatd  48771  intubeu  48772  unilbeu  48773  setrecsres  48932