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  4243  exmidundif  4250  exmidundifim  4251  dmcosseq  4950  relfld  5211  imadif  5354  imain  5356  fimacnv  5709  fo2ndf  6313  tposeq  6333  tfrlemibfn  6414  tfrlemi14d  6419  tfr1onlembfn  6430  tfri1dALT  6437  tfrcllembfn  6443  dcdifsnid  6590  fisbth  6980  en2eqpr  7004  exmidpw  7005  exmidpweq  7006  undifdcss  7020  nnnninfeq2  7231  en2other2  7304  exmidontriimlem3  7335  addnqpr  7674  mulnqpr  7690  distrprg  7701  ltexpri  7726  addcanprg  7729  recexprlemex  7750  aptipr  7754  cauappcvgprlemladd  7771  fzopth  10183  fzosplit  10301  fzouzsplit  10303  zsupssdc  10381  frecuzrdgtcl  10557  frecuzrdgdomlem  10562  ccatrn  11065  phimullem  12547  structcnvcnv  12848  imasaddfnlemg  13146  gsumvallem2  13325  trivsubgd  13536  trivsubgsnd  13537  trivnsgd  13553  kerf1ghm  13610  conjnmz  13615  lspun  14164  lspsn  14178  lspsnneg  14182  lsp0  14185  lsslsp  14191  mulgrhm2  14372  znrrg  14422  eltg4i  14527  unitg  14534  tgtop  14540  tgidm  14546  basgen  14552  2basgeng  14554  epttop  14562  ntrin  14596  isopn3  14597  neiuni  14633  tgrest  14641  resttopon  14643  rest0  14651  txdis  14749  hmeontr  14785  xmettx  14982  findset  15885  pwtrufal  15938  pwf1oexmid  15940