Theorem eqssd 3109

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

Syntax hints:   -> wi 4   = wceq 1331   C_ wss 3066

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079

This theorem is referenced by:  eqrd  3110  eqelssd  3111  unissel  3760  intmin  3786  int0el  3796  pwntru  4117  exmidundif  4124  exmidundifim  4125  dmcosseq  4805  relfld  5062  imadif  5198  imain  5200  fimacnv  5542  fo2ndf  6117  tposeq  6137  tfrlemibfn  6218  tfrlemi14d  6223  tfr1onlembfn  6234  tfri1dALT  6241  tfrcllembfn  6247  dcdifsnid  6393  fisbth  6770  en2eqpr  6794  exmidpw  6795  undifdcss  6804  en2other2  7045  addnqpr  7362  mulnqpr  7378  distrprg  7389  ltexpri  7414  addcanprg  7417  recexprlemex  7438  aptipr  7442  cauappcvgprlemladd  7459  fzopth  9834  fzosplit  9947  fzouzsplit  9949  frecuzrdgtcl  10178  frecuzrdgdomlem  10183  phimullem  11890  structcnvcnv  11964  eltg4i  12213  unitg  12220  tgtop  12226  tgidm  12232  basgen  12238  2basgeng  12240  epttop  12248  ntrin  12282  isopn3  12283  neiuni  12319  tgrest  12327  resttopon  12329  rest0  12337  txdis  12435  hmeontr  12471  xmettx  12668  findset  13132  pwtrufal  13181  pwf1oexmid  13183