Theorem eqssd 3210

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

Syntax hints:   -> wi 4   = wceq 1373   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  eqrd  3211  eqelssd  3212  unissel  3879  intmin  3905  int0el  3915  pwntru  4244  exmidundif  4251  exmidundifim  4252  dmcosseq  4951  relfld  5212  imadif  5355  imain  5357  fimacnv  5711  fo2ndf  6315  tposeq  6335  tfrlemibfn  6416  tfrlemi14d  6421  tfr1onlembfn  6432  tfri1dALT  6439  tfrcllembfn  6445  dcdifsnid  6592  fisbth  6982  en2eqpr  7006  exmidpw  7007  exmidpweq  7008  undifdcss  7022  nnnninfeq2  7233  en2other2  7306  exmidontriimlem3  7337  addnqpr  7676  mulnqpr  7692  distrprg  7703  ltexpri  7728  addcanprg  7731  recexprlemex  7752  aptipr  7756  cauappcvgprlemladd  7773  fzopth  10185  fzosplit  10303  fzouzsplit  10305  zsupssdc  10383  frecuzrdgtcl  10559  frecuzrdgdomlem  10564  ccatrn  11068  phimullem  12580  structcnvcnv  12881  imasaddfnlemg  13179  gsumvallem2  13358  trivsubgd  13569  trivsubgsnd  13570  trivnsgd  13586  kerf1ghm  13643  conjnmz  13648  lspun  14197  lspsn  14211  lspsnneg  14215  lsp0  14218  lsslsp  14224  mulgrhm2  14405  znrrg  14455  eltg4i  14560  unitg  14567  tgtop  14573  tgidm  14579  basgen  14585  2basgeng  14587  epttop  14595  ntrin  14629  isopn3  14630  neiuni  14666  tgrest  14674  resttopon  14676  rest0  14684  txdis  14782  hmeontr  14818  xmettx  15015  findset  15918  pwtrufal  15971  pwf1oexmid  15973