Theorem eqssd 3478

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 3476	. 2 |- ( A = B <-> ( A C_ B /\ B C_ A ) )
4	1, 2, 3	sylanbrc 668	1 |- ( ph -> A = B )

Syntax hints:   -> wi 4   = wceq 1437   C_ wss 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-in 3440  df-ss 3447

This theorem is referenced by:  eqrd  3479  uneqdifeq  3881  unissel  4243  intmin  4269  unissint  4274  int0el  4281  dmcosseq  5108  sofld  5296  relfld  5373  preddowncl  5418  wfi  5424  tz7.7  5460  fimacnv  6019  knatar  6255  sorpssuni  6586  sorpssint  6587  onint  6628  fo2ndf  6906  suppimacnv  6928  tposeq  6975  wfrlem10  7045  onfununi  7060  tfrlem15  7110  oaass  7262  odi  7280  omass  7281  oelim2  7296  oeeui  7303  nnawordex  7338  oaabslem  7344  oaabs2  7346  omabslem  7347  omabs  7348  uniinqs  7443  sucdom2  7766  fineqv  7785  dffi2  7935  fiuni  7940  dffi3  7943  ordtypelem9  8039  ordtypelem10  8040  oismo  8053  hartogslem1  8055  ixpiunwdom  8104  cantnfp1lem3  8182  oemapvali  8186  cantnf  8195  r1val1  8254  rankval3b  8294  rankunb  8318  rankuni2b  8321  rankr1id  8330  rankc2  8339  rankxplim  8347  tcrank  8352  carden2b  8398  harval2  8428  en2other2  8437  infpwfien  8489  coflim  8687  cfcof  8700  cfidm  8701  isf32lem2  8780  fin1a2lem11  8836  fin1a2lem13  8838  ttukeylem7  8941  fpwwe2  9064  winafp  9118  wuncidm  9167  wuncval2  9168  tskuni  9204  grur1  9241  distrpr  9449  prlem934  9454  ltexpri  9464  reclem4pr  9471  fzopth  11829  fzosplit  11945  fzouzsplit  11947  ccatrn  12716  cotrtrclfv  13055  dmtrclfv  13061  dfrtrcl2  13104  phimullem  14705  prmreclem5  14842  structcnvcnv  15110  imasaddfnlem  15412  imasvscafn  15421  mrcuni  15505  mressmrcd  15511  submrc  15512  ssceq  15709  rescabs  15716  setcepi  15961  clatl  16340  ipopos  16384  psdmrn  16431  psssdm2  16439  dirdm  16458  gsumress  16497  gsumvallem2  16597  gsumwspan  16608  cycsubg  16823  conjnmz  16894  pmtrprfv  17072  symggen  17089  odf1o2  17200  gex1  17221  sylow2alem1  17247  sylow3lem3  17259  lsmidm  17292  lsmss1  17294  lsmss2  17296  lsmmod  17303  lsmdisj  17309  lsmdisj2  17310  cntzcmn  17458  prmcyg  17506  dmdprdd  17609  dprdspan  17638  dprdres  17639  dprdz  17641  subgdmdprd  17645  subgdprd  17646  dprddisj2  17650  dprd2dlem1  17652  dprd2da  17653  dmdprdsplit2lem  17656  dprdsplit  17659  ablfacrp  17677  pgpfac1lem3  17688  kerf1hrm  17949  isdrng2  17963  issubdrg  18011  lspun  18188  lspsn  18203  lspsnneg  18207  lsp0  18210  lsslsp  18216  lmhmlsp  18250  lspextmo  18257  lsmsp  18287  lspprabs  18296  lspsnvs  18315  lspdisj  18326  lsmcv  18342  lspsnat  18346  lsppratlem6  18353  lspprat  18354  lbsextlem4  18362  lidl1el  18420  drngnidl  18431  lidldvgen  18457  fidomndrng  18509  mplbas2  18672  cnsubrg  19006  mulgrhm2  19047  znrrg  19113  ocvin  19214  ocvlsp  19216  mrccss  19234  pjfo  19255  obs2ss  19269  frlmsslsp  19331  topsn  19927  eltg4i  19952  unitg  19959  tgtop  19966  tgidm  19973  en2top  19978  basgen  19981  2basgen  19983  fctop  19996  cctop  19998  ppttop  19999  epttop  20001  ntrin  20053  isopn3  20059  opnnei  20113  neiuni  20115  maxlp  20140  clslp  20141  tgrest  20152  resttopon  20154  rest0  20162  restfpw  20172  restcls  20174  restntr  20175  ordtbas2  20184  ordtbas  20185  ordtrest2  20197  cmpcov2  20382  tgcmp  20393  cmpcld  20394  uncmp  20395  cmpfi  20400  2ndcsep  20451  dis2ndc  20452  restnlly  20474  dislly  20489  comppfsc  20524  kgentopon  20530  kgencmp  20537  kgenidm  20539  iskgen2  20540  kgencn3  20550  ptuni2  20568  ptbasfi  20573  xkouni  20591  txcls  20596  ptclsg  20607  txdis  20624  txindis  20626  txcmplem2  20634  xkopt  20647  txcon  20681  qtopval2  20688  qtopuni  20694  qtoprest  20709  qtopomap  20710  qtopcmap  20711  kqsat  20723  kqcldsat  20725  hmeocls  20760  hmeontr  20761  hmphdis  20788  fgfil  20867  fgabs  20871  trfil1  20878  fgtr  20882  trfg  20883  uzrest  20889  ufilmax  20899  ufileu  20911  filufint  20912  ufildom1  20918  rnelfm  20945  flimfil  20961  uffclsflim  21023  alexsublem  21036  alexsubALTlem3  21041  alexsubALT  21043  ptcmplem2  21045  ptcmplem3  21046  tgpconcompeqg  21103  haustsms2  21128  tgptsmscls  21141  ust0  21211  ustbas2  21217  restutopopn  21230  unirnblps  21411  unirnbl  21412  iccntr  21816  pi1xfrcnv  22065  clsocv  22198  cfilfcls  22221  equivcmet  22262  pjth  22370  hlhil  22374  evthicc2  22388  ovolshft  22441  volsup  22486  dyadmbllem  22534  opnmbllem  22536  mbfconstlem  22562  itg11  22626  limciun  22826  dvidlem  22847  dvnres  22862  cpnord  22866  dvaddf  22873  dvmulf  22874  dvcmulf  22876  dvcof  22879  dvcj  22881  dvrec  22886  dvmptcmul  22895  dvcnv  22906  dvcnvre  22948  ftc1cn  22972  plyco0  23123  taylthlem1  23305  taylthlem2  23306  ulmdvlem3  23334  ulmdv  23335  pserdv  23361  wilthlem2  23971  ppisval  24007  ppisval2  24008  ppinprm  24056  chtnprm  24058  umgraex  25027  ubthlem1  26488  pjhth  27022  ococin  27037  chsupsn  27042  ssjo  27076  chabs1  27145  spansncvi  27281  mdslj1i  27948  mdslj2i  27949  atomli  28011  atcvatlem  28014  atcvat3i  28025  sumdmdlem  28047  reff  28655  cmpcref  28666  xpinpreima2  28702  ordtrest2NEW  28718  sigagenid  28962  imambfm  29073  dya2iocuni  29094  bnj1136  29795  bnj1398  29832  bnj1408  29834  bnj1498  29859  sconpi1  29951  cvmsss2  29986  cvmliftlem15  30010  dftrpred3g  30462  trpredpo  30464  frind  30469  sltval2  30531  nofulllem5  30581  altopthsn  30714  opnbnd  30967  opnregcld  30972  cldregopn  30973  fnessref  30999  neibastop1  31001  topmeet  31006  topjoin  31007  fnemeet1  31008  fnejoin1  31010  dissneqlem  31677  poimirlem13  31861  poimirlem14  31862  poimirlem15  31863  opnmbllem0  31884  ftc1cnnc  31924  fdc  31982  sstotbnd2  32014  isbnd2  32023  totbndbnd  32029  prdstotbnd  32034  heibor1  32050  1idl  32167  igenval2  32207  lshpdisj  32466  lssats  32491  lsatcvat3  32531  lkrlsp  32581  lshpset2N  32598  lfl1dim  32600  lfl1dim2N  32601  lkrpssN  32642  paddass  33316  paddidm  33319  pmod1i  33326  pmapjat1  33331  pclbtwnN  33375  pclunN  33376  paddunN  33405  pclfinclN  33428  cdleme50rnlem  34024  dihjust  34698  dihmeetlem1N  34771  dihglblem5apreN  34772  dihmeetlem13N  34800  dochocsp  34860  dochdmj1  34871  dochnoncon  34872  dihjatb  34897  dihjat1lem  34909  lcfl9a  34986  lclkrlem2s  35006  lclkrlem2v  35009  mapdrvallem3  35127  mapdunirnN  35131  mapdin  35143  mapdlsm  35145  baerlem3lem2  35191  baerlem5alem2  35192  baerlem5blem2  35193  hdmaprnN  35348  hgmaprnN  35385  hdmaplkr  35397  rntrclfvOAI  35446  ismrcd1  35453  ismrcd2  35454  isnacs3  35465  nacsfix  35467  kercvrlsm  35855  pwssplit4  35861  hbtlem5  35901  rgspnid  35952  iocinico  36010  cbviuneq12df  36107  dfrcl2  36120  dftrcl3  36166  brtrclfv2  36173  dfrtrcl3  36179  nzin  36519  founiiun  37284  founiiun0  37303  disjf1o  37304  iuneqfzuz  37382  icoiccdif  37425  lptioo2  37498  lptioo1  37499  fourierdlem79  37836  intsaluni  37956  sge0f1o  37979  iundjiun  38028  meadjiunlem  38033  caragenuni  38062  caragendifcl  38065  fzoopth  38659  lspeqlco  39296