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

Theorem eqssd 3084
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 3082 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
41, 2, 3sylanbrc 413 1  |-  ( ph  ->  A  =  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1316    C_ wss 3041
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-11 1469  ax-4 1472  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099
This theorem depends on definitions:  df-bi 116  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-in 3047  df-ss 3054
This theorem is referenced by:  eqrd  3085  eqelssd  3086  unissel  3735  intmin  3761  int0el  3771  pwntru  4092  exmidundif  4099  exmidundifim  4100  dmcosseq  4780  relfld  5037  imadif  5173  imain  5175  fimacnv  5517  fo2ndf  6092  tposeq  6112  tfrlemibfn  6193  tfrlemi14d  6198  tfr1onlembfn  6209  tfri1dALT  6216  tfrcllembfn  6222  dcdifsnid  6368  fisbth  6745  en2eqpr  6769  exmidpw  6770  undifdcss  6779  en2other2  7020  addnqpr  7337  mulnqpr  7353  distrprg  7364  ltexpri  7389  addcanprg  7392  recexprlemex  7413  aptipr  7417  cauappcvgprlemladd  7434  fzopth  9796  fzosplit  9909  fzouzsplit  9911  frecuzrdgtcl  10140  frecuzrdgdomlem  10145  phimullem  11812  structcnvcnv  11886  eltg4i  12135  unitg  12142  tgtop  12148  tgidm  12154  basgen  12160  2basgeng  12162  epttop  12170  ntrin  12204  isopn3  12205  neiuni  12241  tgrest  12249  resttopon  12251  rest0  12259  txdis  12357  hmeontr  12393  xmettx  12590  findset  13039  pwtrufal  13088  pwf1oexmid  13090
  Copyright terms: Public domain W3C validator