Theorem eqssd 3080

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

Syntax hints:   -> wi 4   = wceq 1314   C_ wss 3037

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097

This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3043  df-ss 3050

This theorem is referenced by:  eqrd  3081  eqelssd  3082  unissel  3731  intmin  3757  int0el  3767  pwntru  4082  exmidundif  4089  exmidundifim  4090  dmcosseq  4768  relfld  5025  imadif  5161  imain  5163  fimacnv  5503  fo2ndf  6078  tposeq  6098  tfrlemibfn  6179  tfrlemi14d  6184  tfr1onlembfn  6195  tfri1dALT  6202  tfrcllembfn  6208  dcdifsnid  6354  fisbth  6730  en2eqpr  6754  exmidpw  6755  undifdcss  6764  en2other2  7000  addnqpr  7317  mulnqpr  7333  distrprg  7344  ltexpri  7369  addcanprg  7372  recexprlemex  7393  aptipr  7397  cauappcvgprlemladd  7414  fzopth  9734  fzosplit  9847  fzouzsplit  9849  frecuzrdgtcl  10078  frecuzrdgdomlem  10083  phimullem  11746  structcnvcnv  11818  eltg4i  12067  unitg  12074  tgtop  12080  tgidm  12086  basgen  12092  2basgeng  12094  epttop  12102  ntrin  12136  isopn3  12137  neiuni  12173  tgrest  12181  resttopon  12183  rest0  12191  txdis  12288  xmettx  12499  findset  12833  pwtrufal  12882  pwf1oexmid  12884