Theorem eqssd 3174

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

Syntax hints:   -> wi 4   = wceq 1353   C_ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  eqrd  3175  eqelssd  3176  unissel  3840  intmin  3866  int0el  3876  pwntru  4201  exmidundif  4208  exmidundifim  4209  dmcosseq  4900  relfld  5159  imadif  5298  imain  5300  fimacnv  5647  fo2ndf  6230  tposeq  6250  tfrlemibfn  6331  tfrlemi14d  6336  tfr1onlembfn  6347  tfri1dALT  6354  tfrcllembfn  6360  dcdifsnid  6507  fisbth  6885  en2eqpr  6909  exmidpw  6910  exmidpweq  6911  undifdcss  6924  nnnninfeq2  7129  en2other2  7197  exmidontriimlem3  7224  addnqpr  7562  mulnqpr  7578  distrprg  7589  ltexpri  7614  addcanprg  7617  recexprlemex  7638  aptipr  7642  cauappcvgprlemladd  7659  fzopth  10063  fzosplit  10179  fzouzsplit  10181  frecuzrdgtcl  10414  frecuzrdgdomlem  10419  zsupssdc  11957  phimullem  12227  structcnvcnv  12480  imasaddfnlemg  12740  trivsubgd  13065  trivsubgsnd  13066  trivnsgd  13082  lspun  13493  lspsn  13507  lspsnneg  13511  lsp0  13514  lsslsp  13520  eltg4i  13640  unitg  13647  tgtop  13653  tgidm  13659  basgen  13665  2basgeng  13667  epttop  13675  ntrin  13709  isopn3  13710  neiuni  13746  tgrest  13754  resttopon  13756  rest0  13764  txdis  13862  hmeontr  13898  xmettx  14095  findset  14782  pwtrufal  14832  pwf1oexmid  14834