Theorem eqssd 3241

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

Syntax hints:   -> wi 4   = wceq 1395   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  eqrd  3242  eqelssd  3243  unissel  3917  intmin  3943  int0el  3953  pwntru  4284  exmidundif  4291  exmidundifim  4292  dmcosseq  4999  relfld  5260  imadif  5404  imain  5406  fimacnv  5769  fo2ndf  6384  tposeq  6404  tfrlemibfn  6485  tfrlemi14d  6490  tfr1onlembfn  6501  tfri1dALT  6508  tfrcllembfn  6514  dcdifsnid  6663  fisbth  7058  en2eqpr  7085  exmidpw  7086  exmidpweq  7087  undifdcss  7101  nnnninfeq2  7312  en2other2  7390  exmidontriimlem3  7421  pw1m  7425  addnqpr  7764  mulnqpr  7780  distrprg  7791  ltexpri  7816  addcanprg  7819  recexprlemex  7840  aptipr  7844  cauappcvgprlemladd  7861  fzopth  10274  fzosplit  10392  fzouzsplit  10394  zsupssdc  10475  frecuzrdgtcl  10651  frecuzrdgdomlem  10656  ccatrn  11162  phimullem  12768  structcnvcnv  13069  imasaddfnlemg  13368  gsumvallem2  13547  trivsubgd  13758  trivsubgsnd  13759  trivnsgd  13775  kerf1ghm  13832  conjnmz  13837  lspun  14387  lspsn  14401  lspsnneg  14405  lsp0  14408  lsslsp  14414  mulgrhm2  14595  znrrg  14645  eltg4i  14750  unitg  14757  tgtop  14763  tgidm  14769  basgen  14775  2basgeng  14777  epttop  14785  ntrin  14819  isopn3  14820  neiuni  14856  tgrest  14864  resttopon  14866  rest0  14874  txdis  14972  hmeontr  15008  xmettx  15205  findset  16417  pwtrufal  16476  pwf1oexmid  16478