Theorem eqssd 3197

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

Syntax hints:   -> wi 4   = wceq 1364   C_ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  eqrd  3198  eqelssd  3199  unissel  3865  intmin  3891  int0el  3901  pwntru  4229  exmidundif  4236  exmidundifim  4237  dmcosseq  4934  relfld  5195  imadif  5335  imain  5337  fimacnv  5688  fo2ndf  6282  tposeq  6302  tfrlemibfn  6383  tfrlemi14d  6388  tfr1onlembfn  6399  tfri1dALT  6406  tfrcllembfn  6412  dcdifsnid  6559  fisbth  6941  en2eqpr  6965  exmidpw  6966  exmidpweq  6967  undifdcss  6981  nnnninfeq2  7190  en2other2  7258  exmidontriimlem3  7285  addnqpr  7623  mulnqpr  7639  distrprg  7650  ltexpri  7675  addcanprg  7678  recexprlemex  7699  aptipr  7703  cauappcvgprlemladd  7720  fzopth  10130  fzosplit  10247  fzouzsplit  10249  frecuzrdgtcl  10486  frecuzrdgdomlem  10491  zsupssdc  12094  phimullem  12366  structcnvcnv  12637  imasaddfnlemg  12900  gsumvallem2  13068  trivsubgd  13273  trivsubgsnd  13274  trivnsgd  13290  kerf1ghm  13347  conjnmz  13352  lspun  13901  lspsn  13915  lspsnneg  13919  lsp0  13922  lsslsp  13928  mulgrhm2  14109  znrrg  14159  eltg4i  14234  unitg  14241  tgtop  14247  tgidm  14253  basgen  14259  2basgeng  14261  epttop  14269  ntrin  14303  isopn3  14304  neiuni  14340  tgrest  14348  resttopon  14350  rest0  14358  txdis  14456  hmeontr  14492  xmettx  14689  findset  15507  pwtrufal  15558  pwf1oexmid  15560