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

Theorem eqssd 2939
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 (φAB)
eqssd.2 (φBA)
Assertion
Ref Expression
eqssd (φA = B)

Proof of Theorem eqssd
StepHypRef Expression
1 eqssd.1 . 2 (φAB)
2 eqssd.2 . 2 (φBA)
3 eqss 2937 . 2 (A = B ↔ (AB BA))
41, 2, 3sylanbrc 396 1 (φA = B)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228  wss 2894
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1316  ax-7 1317  ax-gen 1318  ax-ie1 1363  ax-ie2 1364  ax-8 1376  ax-11 1378  ax-4 1381  ax-17 1400  ax-i9 1404  ax-ial 1409  ax-i5r 1410  ax-ext 2004
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1628  df-clab 2009  df-cleq 2015  df-clel 2018  df-in 2901  df-ss 2908
This theorem is referenced by:  eqrd  2940  unissel  3583  intmin  3609  int0el  3619  dmcosseq  4530  relfld  4773  imadif  4905  imain  4907  fimacnv  5221  fo2ndf  5771  tposeq  5784  tfrlemibfn  5863  tfrlemi14d  5868  distrprg  6427  ltexpri  6450  addcanprg  6453  recexprlemex  6471  findset  7167
  Copyright terms: Public domain W3C validator