Theorem eqssd 3325

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	|- ( ph -> A C_ B )
eqssd.2	|- ( ph -> B C_ A )

Assertion

Ref	Expression
eqssd	|- ( ph -> A = B )

Proof of Theorem eqssd

Step	Hyp	Ref	Expression
1		eqssd.1	. 2 |- ( ph -> A C_ B )
2		eqssd.2	. 2 |- ( ph -> B C_ A )
3		eqss 3323	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
4	1, 2, 3	sylanbrc 646	1 |- ( ph -> A = B )

Syntax hints:   -> wi 4   = wceq 1649   C_ wss 3280

This theorem is referenced by:  eqrd  3326  uneqdifeq  3676  unissel  4004  intmin  4030  unissint  4034  int0el  4041  tz7.7  4567  reusv6OLD  4693  onint  4734  dmcosseq  5096  sofld  5277  relfld  5354  fimacnv  5821  knatar  6039  fo2ndf  6412  tposeq  6440  sorpssuni  6490  sorpssint  6491  onfununi  6562  tfrlem15  6612  oaass  6763  odi  6781  omass  6782  oelim2  6797  oeeui  6804  nnawordex  6839  oaabslem  6845  oaabs2  6847  omabslem  6848  omabs  6849  uniinqs  6943  sucdom2  7262  fineqv  7283  dffi2  7386  fiuni  7391  dffi3  7394  ordtypelem9  7451  ordtypelem10  7452  oismo  7465  hartogslem1  7467  ixpiunwdom  7515  cantnfp1lem3  7592  oemapvali  7596  cantnf  7605  r1val1  7668  rankval3b  7708  rankunb  7732  rankuni2b  7735  rankr1id  7744  rankc2  7753  rankxplim  7759  tcrank  7764  carden2b  7810  harval2  7840  infpwfien  7899  coflim  8097  cfcof  8110  cfidm  8111  isf32lem2  8190  fin1a2lem11  8246  fin1a2lem13  8248  ttukeylem7  8351  fpwwe2  8474  winafp  8528  wuncidm  8577  wuncval2  8578  tskuni  8614  grur1  8651  distrpr  8861  prlem934  8866  ltexpri  8876  reclem4pr  8883  fzopth  11045  fzosplit  11121  fzouzsplit  11123  phimullem  13123  prmreclem5  13243  structcnvcnv  13435  imasaddfnlem  13708  imasvscafn  13717  mrcuni  13801  mressmrcd  13807  submrc  13808  ssceq  13981  rescabs  13988  setcepi  14198  ipopos  14541  psdmrn  14594  psssdm2  14602  dirdm  14634  gsumvallem2  14727  gsumress  14732  gsumwspan  14746  cycsubg  14923  conjnmz  14994  odf1o2  15162  gex1  15180  sylow2alem1  15206  sylow3lem3  15218  lsmidm  15251  lsmss1  15253  lsmss2  15255  lsmmod  15262  lsmdisj  15268  lsmdisj2  15269  cntzcmn  15414  prmcyg  15458  dmdprdd  15515  dprdspan  15540  dprdres  15541  dprdz  15543  subgdmdprd  15547  subgdprd  15548  dprddisj2  15552  dprd2dlem1  15554  dprd2da  15555  dmdprdsplit2lem  15558  dprdsplit  15561  ablfacrp  15579  pgpfac1lem3  15590  isdrng2  15800  issubdrg  15848  lspun  16018  lspsn  16033  lspsnneg  16037  lsp0  16040  lsslsp  16046  lmhmlsp  16080  lspextmo  16087  lsmsp  16113  lspprabs  16122  lspsnvs  16141  lspdisj  16152  lsmcv  16168  lspsnat  16172  lsppratlem6  16179  lspprat  16180  lbsextlem4  16188  lidl1el  16244  drngnidl  16255  lidldvgen  16281  fidomndrng  16322  mplbas2  16486  cnsubrg  16714  mulgrhm2  16743  znrrg  16801  ocvin  16856  ocvlsp  16858  mrccss  16876  pjfo  16897  obs2ss  16911  topsn  16955  eltg4i  16980  tgtop  16993  tgidm  17000  en2top  17005  basgen  17008  2basgen  17010  fctop  17023  cctop  17025  ppttop  17026  epttop  17028  ntrin  17080  isopn3  17085  opnnei  17139  neiuni  17141  maxlp  17165  clslp  17166  tgrest  17177  resttopon  17179  rest0  17187  restfpw  17197  restcls  17199  restntr  17200  ordtbas2  17209  ordtbas  17210  ordtrest2  17222  cmpcov2  17407  tgcmp  17418  cmpcld  17419  uncmp  17420  cmpfi  17425  2ndcsep  17475  dis2ndc  17476  restnlly  17498  dislly  17513  kgentopon  17523  kgencmp  17530  kgenidm  17532  iskgen2  17533  kgencn3  17543  ptuni2  17561  ptbasfi  17566  xkouni  17584  txcls  17589  ptclsg  17600  txdis  17617  txindis  17619  txcmplem2  17627  xkopt  17640  txcon  17674  qtopval2  17681  qtopuni  17687  qtoprest  17702  qtopomap  17703  qtopcmap  17704  kqsat  17716  kqcldsat  17718  hmeocls  17753  hmeontr  17754  hmphdis  17781  fgfil  17860  fgabs  17864  trfil1  17871  fgtr  17875  trfg  17876  uzrest  17882  ufilmax  17892  ufileu  17904  filufint  17905  ufildom1  17911  rnelfm  17938  flimfil  17954  uffclsflim  18016  alexsublem  18028  alexsubALTlem3  18033  alexsubALT  18035  ptcmplem2  18037  ptcmplem3  18038  tgpconcompeqg  18094  haustsms2  18119  tgptsmscls  18132  ust0  18202  ustbas2  18208  restutopopn  18221  unirnblps  18402  unirnbl  18403  iccntr  18805  pi1xfrcnv  19035  clsocv  19157  cfilfcls  19180  equivcmet  19221  pjth  19293  hlhil  19297  evthicc2  19310  ovolshft  19360  volsup  19403  dyadmbllem  19444  opnmbllem  19446  mbfconstlem  19474  itg11  19536  limciun  19734  dvidlem  19755  dvnres  19770  cpnord  19774  dvaddf  19781  dvmulf  19782  dvcmulf  19784  dvcof  19787  dvcj  19789  dvrec  19794  dvmptcmul  19803  dvcnv  19814  dvcnvre  19856  ftc1cn  19880  plyco0  20064  taylthlem1  20242  taylthlem2  20243  ulmdvlem3  20271  ulmdv  20272  pserdv  20298  wilthlem2  20805  ppisval  20839  ppisval2  20840  ppinprm  20888  chtnprm  20890  umgraex  21311  ubthlem1  22325  pjhth  22848  ococin  22863  chsupsn  22868  ssjo  22902  chabs1  22971  spansncvi  23107  mdslj1i  23775  mdslj2i  23776  atomli  23838  atcvatlem  23841  atcvat3i  23852  sumdmdlem  23874  kerf1hrm  24215  xpinpreima2  24258  sigagenid  24487  imambfm  24565  dya2iocuni  24586  sconpi1  24879  cvmsss2  24914  cvmliftlem15  24938  dfrtrcl2  25101  preddowncl  25410  wfi  25421  dftrpred3g  25450  trpredpo  25452  frind  25457  wfrlem10  25479  sltval2  25524  nofulllem5  25574  altopthsn  25710  mblfinlem  26143  ftc1cnnc  26178  opnbnd  26218  opnregcld  26223  cldregopn  26224  fnessref  26263  comppfsc  26277  neibastop1  26278  topmeet  26283  topjoin  26284  fnemeet1  26285  fnejoin1  26287  fdc  26339  sstotbnd2  26373  isbnd2  26382  totbndbnd  26388  prdstotbnd  26393  heibor1  26409  1idl  26526  igenval2  26566  ismrcd1  26642  ismrcd2  26643  isnacs3  26654  nacsfix  26656  kercvrlsm  27049  pwssplit4  27059  frlmsslsp  27116  hbtlem5  27200  rgspnid  27245  en2other2  27250  pmtrprfv  27264  symggen  27279  bnj1136  29072  bnj1398  29109  bnj1408  29111  bnj1498  29136  lshpdisj  29470  lssats  29495  lsatcvat3  29535  lkrlsp  29585  lshpset2N  29602  lfl1dim  29604  lfl1dim2N  29605  lkrpssN  29646  paddass  30320  paddidm  30323  pmod1i  30330  pmapjat1  30335  pclbtwnN  30379  pclunN  30380  paddunN  30409  pclfinclN  30432  cdleme50rnlem  31026  dihjust  31700  dihmeetlem1N  31773  dihglblem5apreN  31774  dihmeetlem13N  31802  dochocsp  31862  dochdmj1  31873  dochnoncon  31874  dihjatb  31899  dihjat1lem  31911  lcfl9a  31988  lclkrlem2s  32008  lclkrlem2v  32011  mapdrvallem3  32129  mapdunirnN  32133  mapdin  32145  mapdlsm  32147  baerlem3lem2  32193  baerlem5alem2  32194  baerlem5blem2  32195  hdmaprnN  32350  hgmaprnN  32387  hdmaplkr  32399

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294