ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  eqssd Unicode version

Theorem eqssd 2989
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
StepHypRef Expression
1 eqssd.1 . 2  |-  ( ph  ->  A  C_  B )
2 eqssd.2 . 2  |-  ( ph  ->  B  C_  A )
3 eqss 2987 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3sylanbrc 402 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1259    C_ wss 2944
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2951  df-ss 2958
This theorem is referenced by:  eqrd  2990  unissel  3636  intmin  3662  int0el  3672  dmcosseq  4630  relfld  4873  imadif  5006  imain  5008  fimacnv  5323  fo2ndf  5875  tposeq  5892  tfrlemibfn  5972  tfrlemi14d  5977  nndifsnid  6110  fidifsnid  6362  fisbth  6370  addnqpr  6716  mulnqpr  6732  distrprg  6743  ltexpri  6768  addcanprg  6771  recexprlemex  6792  aptipr  6796  cauappcvgprlemladd  6813  fzopth  9025  fzosplit  9134  fzouzsplit  9136  frecuzrdgfn  9361  findset  10436
  Copyright terms: Public domain W3C validator