Theorem eqssd 3448

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

Syntax hints:   -> wi 4   = wceq 1443   C_ wss 3403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1668  ax-4 1681  ax-5 1757  ax-6 1804  ax-7 1850  ax-10 1914  ax-11 1919  ax-12 1932  ax-13 2090  ax-ext 2430

This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1446  df-ex 1663  df-nf 1667  df-sb 1797  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3410  df-ss 3417

This theorem is referenced by:  eqrd  3449  uneqdifeq  3855  unissel  4227  intmin  4253  unissint  4258  int0el  4265  dmcosseq  5095  sofld  5283  relfld  5360  preddowncl  5406  wfi  5412  tz7.7  5448  fimacnv  6010  knatar  6246  sorpssuni  6577  sorpssint  6578  onint  6619  fo2ndf  6900  suppimacnv  6922  tposeq  6972  wfrlem10  7042  onfununi  7057  tfrlem15  7107  oaass  7259  odi  7277  omass  7278  oelim2  7293  oeeui  7300  nnawordex  7335  oaabslem  7341  oaabs2  7343  omabslem  7344  omabs  7345  uniinqs  7440  sucdom2  7765  fineqv  7784  dffi2  7934  fiuni  7939  dffi3  7942  ordtypelem9  8038  ordtypelem10  8039  oismo  8052  hartogslem1  8054  ixpiunwdom  8103  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  8490  coflim  8688  cfcof  8701  cfidm  8702  isf32lem2  8781  fin1a2lem11  8837  fin1a2lem13  8839  ttukeylem7  8942  fpwwe2  9065  winafp  9119  wuncidm  9168  wuncval2  9169  tskuni  9205  grur1  9242  distrpr  9450  prlem934  9455  ltexpri  9465  reclem4pr  9472  fzopth  11832  fzosplit  11948  fzouzsplit  11950  ccatrn  12730  cotrtrclfv  13069  dmtrclfv  13075  dfrtrcl2  13118  phimullem  14720  prmreclem5  14857  structcnvcnv  15125  imasaddfnlem  15427  imasvscafn  15436  mrcuni  15520  mressmrcd  15526  submrc  15527  ssceq  15724  rescabs  15731  setcepi  15976  clatl  16355  ipopos  16399  psdmrn  16446  psssdm2  16454  dirdm  16473  gsumress  16512  gsumvallem2  16612  gsumwspan  16623  cycsubg  16838  conjnmz  16909  pmtrprfv  17087  symggen  17104  odf1o2  17215  gex1  17236  sylow2alem1  17262  sylow3lem3  17274  lsmidm  17307  lsmss1  17309  lsmss2  17311  lsmmod  17318  lsmdisj  17324  lsmdisj2  17325  cntzcmn  17473  prmcyg  17521  dmdprdd  17624  dprdspan  17653  dprdres  17654  dprdz  17656  subgdmdprd  17660  subgdprd  17661  dprddisj2  17665  dprd2dlem1  17667  dprd2da  17668  dmdprdsplit2lem  17671  dprdsplit  17674  ablfacrp  17692  pgpfac1lem3  17703  kerf1hrm  17964  isdrng2  17978  issubdrg  18026  lspun  18203  lspsn  18218  lspsnneg  18222  lsp0  18225  lsslsp  18231  lmhmlsp  18265  lspextmo  18272  lsmsp  18302  lspprabs  18311  lspsnvs  18330  lspdisj  18341  lsmcv  18357  lspsnat  18361  lsppratlem6  18368  lspprat  18369  lbsextlem4  18377  lidl1el  18435  drngnidl  18446  lidldvgen  18472  fidomndrng  18524  mplbas2  18687  cnsubrg  19021  mulgrhm2  19063  znrrg  19129  ocvin  19230  ocvlsp  19232  mrccss  19250  pjfo  19271  obs2ss  19285  frlmsslsp  19347  topsn  19943  eltg4i  19968  unitg  19975  tgtop  19982  tgidm  19989  en2top  19994  basgen  19997  2basgen  19999  fctop  20012  cctop  20014  ppttop  20015  epttop  20017  ntrin  20069  isopn3  20075  opnnei  20129  neiuni  20131  maxlp  20156  clslp  20157  tgrest  20168  resttopon  20170  rest0  20178  restfpw  20188  restcls  20190  restntr  20191  ordtbas2  20200  ordtbas  20201  ordtrest2  20213  cmpcov2  20398  tgcmp  20409  cmpcld  20410  uncmp  20411  cmpfi  20416  2ndcsep  20467  dis2ndc  20468  restnlly  20490  dislly  20505  comppfsc  20540  kgentopon  20546  kgencmp  20553  kgenidm  20555  iskgen2  20556  kgencn3  20566  ptuni2  20584  ptbasfi  20589  xkouni  20607  txcls  20612  ptclsg  20623  txdis  20640  txindis  20642  txcmplem2  20650  xkopt  20663  txcon  20697  qtopval2  20704  qtopuni  20710  qtoprest  20725  qtopomap  20726  qtopcmap  20727  kqsat  20739  kqcldsat  20741  hmeocls  20776  hmeontr  20777  hmphdis  20804  fgfil  20883  fgabs  20887  trfil1  20894  fgtr  20898  trfg  20899  uzrest  20905  ufilmax  20915  ufileu  20927  filufint  20928  ufildom1  20934  rnelfm  20961  flimfil  20977  uffclsflim  21039  alexsublem  21052  alexsubALTlem3  21057  alexsubALT  21059  ptcmplem2  21061  ptcmplem3  21062  tgpconcompeqg  21119  haustsms2  21144  tgptsmscls  21157  ust0  21227  ustbas2  21233  restutopopn  21246  unirnblps  21427  unirnbl  21428  iccntr  21832  pi1xfrcnv  22081  clsocv  22214  cfilfcls  22237  equivcmet  22278  pjth  22386  hlhil  22390  evthicc2  22404  ovolshft  22457  volsup  22502  dyadmbllem  22550  opnmbllem  22552  mbfconstlem  22578  itg11  22642  limciun  22842  dvidlem  22863  dvnres  22878  cpnord  22882  dvaddf  22889  dvmulf  22890  dvcmulf  22892  dvcof  22895  dvcj  22897  dvrec  22902  dvmptcmul  22911  dvcnv  22922  dvcnvre  22964  ftc1cn  22988  plyco0  23139  taylthlem1  23321  taylthlem2  23322  ulmdvlem3  23350  ulmdv  23351  pserdv  23377  wilthlem2  23987  ppisval  24023  ppisval2  24024  ppinprm  24072  chtnprm  24074  umgraex  25043  ubthlem1  26505  pjhth  27039  ococin  27054  chsupsn  27059  ssjo  27093  chabs1  27162  spansncvi  27298  mdslj1i  27965  mdslj2i  27966  atomli  28028  atcvatlem  28031  atcvat3i  28042  sumdmdlem  28064  reff  28659  cmpcref  28670  xpinpreima2  28706  ordtrest2NEW  28722  sigagenid  28966  imambfm  29077  dya2iocuni  29098  bnj1136  29799  bnj1398  29836  bnj1408  29838  bnj1498  29863  sconpi1  29955  cvmsss2  29990  cvmliftlem15  30014  dftrpred3g  30467  trpredpo  30469  frind  30474  sltval2  30536  nofulllem5  30588  altopthsn  30721  opnbnd  30974  opnregcld  30979  cldregopn  30980  fnessref  31006  neibastop1  31008  topmeet  31013  topjoin  31014  fnemeet1  31015  fnejoin1  31017  dissneqlem  31735  poimirlem13  31946  poimirlem14  31947  poimirlem15  31948  opnmbllem0  31969  ftc1cnnc  32009  fdc  32067  sstotbnd2  32099  isbnd2  32108  totbndbnd  32114  prdstotbnd  32119  heibor1  32135  1idl  32252  igenval2  32292  lshpdisj  32547  lssats  32572  lsatcvat3  32612  lkrlsp  32662  lshpset2N  32679  lfl1dim  32681  lfl1dim2N  32682  lkrpssN  32723  paddass  33397  paddidm  33400  pmod1i  33407  pmapjat1  33412  pclbtwnN  33456  pclunN  33457  paddunN  33486  pclfinclN  33509  cdleme50rnlem  34105  dihjust  34779  dihmeetlem1N  34852  dihglblem5apreN  34853  dihmeetlem13N  34881  dochocsp  34941  dochdmj1  34952  dochnoncon  34953  dihjatb  34978  dihjat1lem  34990  lcfl9a  35067  lclkrlem2s  35087  lclkrlem2v  35090  mapdrvallem3  35208  mapdunirnN  35212  mapdin  35224  mapdlsm  35226  baerlem3lem2  35272  baerlem5alem2  35273  baerlem5blem2  35274  hdmaprnN  35429  hgmaprnN  35466  hdmaplkr  35478  rntrclfvOAI  35527  ismrcd1  35534  ismrcd2  35535  isnacs3  35546  nacsfix  35548  kercvrlsm  35935  pwssplit4  35941  hbtlem5  35981  rgspnid  36032  iocinico  36090  mptrcllem  36214  clcnvlem  36224  dmtrcl  36228  rntrcl  36229  cbviuneq12df  36247  dfrcl2  36260  dftrcl3  36306  brtrclfv2  36313  dfrtrcl3  36319  nzin  36661  founiiun  37440  founiiun0  37459  disjf1o  37460  iuneqfzuz  37552  icoiccdif  37619  iccdificc  37635  lptioo2  37705  lptioo1  37706  fourierdlem79  38043  rrxbasefi  38146  qndenserrn  38162  intsaluni  38182  issalgend  38191  sge0f1o  38218  iundjiun  38292  meadjiunlem  38297  caragenuni  38326  caragendifcl  38329  opnvonmbllem2  38449  fzoopth  39050  upgrex  39170  uvtxnbgr  39456  nbupgruvtxres  39463  cplgruvtxb  39466  cusgredg  39475  lspeqlco  40219