Theorem eqssd 3027

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

Syntax hints:   -> wi 4   = wceq 1285   C_ wss 2984

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-11 1438  ax-4 1441  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-in 2990  df-ss 2997

This theorem is referenced by:  eqrd  3028  unissel  3656  intmin  3682  int0el  3692  exmidundif  3999  dmcosseq  4662  relfld  4913  imadif  5047  imain  5049  fimacnv  5373  fo2ndf  5927  tposeq  5944  tfrlemibfn  6025  tfrlemi14d  6030  tfr1onlembfn  6041  tfri1dALT  6048  tfrcllembfn  6054  dcdifsnid  6195  fisbth  6529  en2eqpr  6550  exmidpw  6551  undifdcss  6560  en2other2  6725  addnqpr  7023  mulnqpr  7039  distrprg  7050  ltexpri  7075  addcanprg  7078  recexprlemex  7099  aptipr  7103  cauappcvgprlemladd  7120  fzopth  9369  fzosplit  9477  fzouzsplit  9479  frecuzrdgtcl  9708  frecuzrdgdomlem  9713  phimullem  10981  findset  11183