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  4283  exmidundif  4290  exmidundifim  4291  dmcosseq  4996  relfld  5257  imadif  5401  imain  5403  fimacnv  5764  fo2ndf  6373  tposeq  6393  tfrlemibfn  6474  tfrlemi14d  6479  tfr1onlembfn  6490  tfri1dALT  6497  tfrcllembfn  6503  dcdifsnid  6650  fisbth  7045  en2eqpr  7069  exmidpw  7070  exmidpweq  7071  undifdcss  7085  nnnninfeq2  7296  en2other2  7374  exmidontriimlem3  7405  pw1m  7409  addnqpr  7748  mulnqpr  7764  distrprg  7775  ltexpri  7800  addcanprg  7803  recexprlemex  7824  aptipr  7828  cauappcvgprlemladd  7845  fzopth  10257  fzosplit  10375  fzouzsplit  10377  zsupssdc  10458  frecuzrdgtcl  10634  frecuzrdgdomlem  10639  ccatrn  11144  phimullem  12747  structcnvcnv  13048  imasaddfnlemg  13347  gsumvallem2  13526  trivsubgd  13737  trivsubgsnd  13738  trivnsgd  13754  kerf1ghm  13811  conjnmz  13816  lspun  14366  lspsn  14380  lspsnneg  14384  lsp0  14387  lsslsp  14393  mulgrhm2  14574  znrrg  14624  eltg4i  14729  unitg  14736  tgtop  14742  tgidm  14748  basgen  14754  2basgeng  14756  epttop  14764  ntrin  14798  isopn3  14799  neiuni  14835  tgrest  14843  resttopon  14845  rest0  14853  txdis  14951  hmeontr  14987  xmettx  15184  findset  16308  pwtrufal  16363  pwf1oexmid  16365