Theorem eqssd 3241

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

Syntax hints:   -> wi 4   = wceq 1395   C_ wss 3197

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqrd  3242  eqelssd  3243  unissel  3917  intmin  3943  int0el  3953  pwntru  4283  exmidundif  4290  exmidundifim  4291  dmcosseq  4996  relfld  5257  imadif  5401  imain  5403  fimacnv  5766  fo2ndf  6379  tposeq  6399  tfrlemibfn  6480  tfrlemi14d  6485  tfr1onlembfn  6496  tfri1dALT  6503  tfrcllembfn  6509  dcdifsnid  6658  fisbth  7053  en2eqpr  7080  exmidpw  7081  exmidpweq  7082  undifdcss  7096  nnnninfeq2  7307  en2other2  7385  exmidontriimlem3  7416  pw1m  7420  addnqpr  7759  mulnqpr  7775  distrprg  7786  ltexpri  7811  addcanprg  7814  recexprlemex  7835  aptipr  7839  cauappcvgprlemladd  7856  fzopth  10269  fzosplit  10387  fzouzsplit  10389  zsupssdc  10470  frecuzrdgtcl  10646  frecuzrdgdomlem  10651  ccatrn  11157  phimullem  12763  structcnvcnv  13064  imasaddfnlemg  13363  gsumvallem2  13542  trivsubgd  13753  trivsubgsnd  13754  trivnsgd  13770  kerf1ghm  13827  conjnmz  13832  lspun  14382  lspsn  14396  lspsnneg  14400  lsp0  14403  lsslsp  14409  mulgrhm2  14590  znrrg  14640  eltg4i  14745  unitg  14752  tgtop  14758  tgidm  14764  basgen  14770  2basgeng  14772  epttop  14780  ntrin  14814  isopn3  14815  neiuni  14851  tgrest  14859  resttopon  14861  rest0  14869  txdis  14967  hmeontr  15003  xmettx  15200  findset  16391  pwtrufal  16450  pwf1oexmid  16452