Theorem eqssd 3245

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

Syntax hints:   -> wi 4   = wceq 1398   C_ wss 3201

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  eqrd  3246  eqelssd  3247  unissel  3927  intmin  3953  int0el  3963  pwntru  4295  exmidundif  4302  exmidundifim  4303  dmcosseq  5010  relfld  5272  imadif  5417  imain  5419  fimacnv  5784  fo2ndf  6401  tposeq  6456  tfrlemibfn  6537  tfrlemi14d  6542  tfr1onlembfn  6553  tfri1dALT  6560  tfrcllembfn  6566  dcdifsnid  6715  fisbth  7115  en2eqpr  7142  exmidpw  7143  exmidpweq  7144  undifdcss  7158  nnnninfeq2  7388  en2other2  7467  exmidontriimlem3  7498  pw1m  7502  addnqpr  7841  mulnqpr  7857  distrprg  7868  ltexpri  7893  addcanprg  7896  recexprlemex  7917  aptipr  7921  cauappcvgprlemladd  7938  fzopth  10358  fzosplit  10476  fzouzsplit  10478  zsupssdc  10561  frecuzrdgtcl  10737  frecuzrdgdomlem  10742  ccatrn  11252  phimullem  12877  structcnvcnv  13178  imasaddfnlemg  13477  gsumvallem2  13656  trivsubgd  13867  trivsubgsnd  13868  trivnsgd  13884  kerf1ghm  13941  conjnmz  13946  lspun  14498  lspsn  14512  lspsnneg  14516  lsp0  14519  lsslsp  14525  mulgrhm2  14706  znrrg  14756  eltg4i  14866  unitg  14873  tgtop  14879  tgidm  14885  basgen  14891  2basgeng  14893  epttop  14901  ntrin  14935  isopn3  14936  neiuni  14972  tgrest  14980  resttopon  14982  rest0  14990  txdis  15088  hmeontr  15124  xmettx  15321  findset  16661  pwtrufal  16719  pwf1oexmid  16721