Theorem eqssd 3244

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

Syntax hints:   -> wi 4   = wceq 1397   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  eqrd  3245  eqelssd  3246  unissel  3922  intmin  3948  int0el  3958  pwntru  4289  exmidundif  4296  exmidundifim  4297  dmcosseq  5004  relfld  5265  imadif  5410  imain  5412  fimacnv  5776  fo2ndf  6392  tposeq  6413  tfrlemibfn  6494  tfrlemi14d  6499  tfr1onlembfn  6510  tfri1dALT  6517  tfrcllembfn  6523  dcdifsnid  6672  fisbth  7072  en2eqpr  7099  exmidpw  7100  exmidpweq  7101  undifdcss  7115  nnnninfeq2  7328  en2other2  7407  exmidontriimlem3  7438  pw1m  7442  addnqpr  7781  mulnqpr  7797  distrprg  7808  ltexpri  7833  addcanprg  7836  recexprlemex  7857  aptipr  7861  cauappcvgprlemladd  7878  fzopth  10296  fzosplit  10414  fzouzsplit  10416  zsupssdc  10499  frecuzrdgtcl  10675  frecuzrdgdomlem  10680  ccatrn  11190  phimullem  12815  structcnvcnv  13116  imasaddfnlemg  13415  gsumvallem2  13594  trivsubgd  13805  trivsubgsnd  13806  trivnsgd  13822  kerf1ghm  13879  conjnmz  13884  lspun  14435  lspsn  14449  lspsnneg  14453  lsp0  14456  lsslsp  14462  mulgrhm2  14643  znrrg  14693  eltg4i  14798  unitg  14805  tgtop  14811  tgidm  14817  basgen  14823  2basgeng  14825  epttop  14833  ntrin  14867  isopn3  14868  neiuni  14904  tgrest  14912  resttopon  14914  rest0  14922  txdis  15020  hmeontr  15056  xmettx  15253  findset  16591  pwtrufal  16649  pwf1oexmid  16651