Theorem eqssd 3255

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

Syntax hints:   -> wi 4   = wceq 1398   C_ wss 3211

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  eqrd  3256  eqelssd  3257  unissel  3943  intmin  3969  int0el  3979  pwntru  4312  exmidundif  4319  exmidundifim  4320  dmcosseq  5029  relfld  5291  imadif  5436  imain  5438  fimacnv  5806  fo2ndf  6423  tposeq  6478  tfrlemibfn  6559  tfrlemi14d  6564  tfr1onlembfn  6575  tfri1dALT  6582  tfrcllembfn  6588  dcdifsnid  6737  fisbth  7140  en2eqpr  7167  exmidpw  7168  exmidpweq  7169  undifdcss  7183  nnnninfeq2  7420  en2other2  7499  exmidontriimlem3  7530  pw1m  7534  addnqpr  7876  mulnqpr  7892  distrprg  7903  ltexpri  7928  addcanprg  7931  recexprlemex  7952  aptipr  7956  cauappcvgprlemladd  7973  fzopth  10395  fzosplit  10513  fzouzsplit  10515  zsupssdc  10598  frecuzrdgtcl  10774  frecuzrdgdomlem  10779  ccatrn  11297  phimullem  12922  structcnvcnv  13228  imasaddfnlemg  13527  gsumvallem2  13706  trivsubgd  13917  trivsubgsnd  13918  trivnsgd  13934  kerf1ghm  13991  conjnmz  13996  lspun  14550  lspsn  14564  lspsnneg  14568  lsp0  14571  lsslsp  14577  mulgrhm2  14758  znrrg  14808  eltg4i  14920  unitg  14927  tgtop  14933  tgidm  14939  basgen  14945  2basgeng  14947  epttop  14955  ntrin  14989  isopn3  14990  neiuni  15026  tgrest  15034  resttopon  15036  rest0  15044  txdis  15142  hmeontr  15178  xmettx  15375  findset  16715  pwtrufal  16771  pwf1oexmid  16773