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

Theorem eqssd 3029
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 (𝜑𝐴𝐵)
eqssd.2 (𝜑𝐵𝐴)
Assertion
Ref Expression
eqssd (𝜑𝐴 = 𝐵)

Proof of Theorem eqssd
StepHypRef Expression
1 eqssd.1 . 2 (𝜑𝐴𝐵)
2 eqssd.2 . 2 (𝜑𝐵𝐴)
3 eqss 3027 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3sylanbrc 408 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  wss 2986
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-11 1440  ax-4 1443  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067
This theorem depends on definitions:  df-bi 115  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-in 2992  df-ss 2999
This theorem is referenced by:  eqrd  3030  unissel  3659  intmin  3685  int0el  3695  exmidundif  4002  dmcosseq  4665  relfld  4916  imadif  5050  imain  5052  fimacnv  5376  fo2ndf  5930  tposeq  5947  tfrlemibfn  6028  tfrlemi14d  6033  tfr1onlembfn  6044  tfri1dALT  6051  tfrcllembfn  6057  dcdifsnid  6198  fisbth  6532  en2eqpr  6553  exmidpw  6554  undifdcss  6563  en2other2  6743  addnqpr  7041  mulnqpr  7057  distrprg  7068  ltexpri  7093  addcanprg  7096  recexprlemex  7117  aptipr  7121  cauappcvgprlemladd  7138  fzopth  9383  fzosplit  9491  fzouzsplit  9493  frecuzrdgtcl  9722  frecuzrdgdomlem  9727  phimullem  10995  findset  11197
  Copyright terms: Public domain W3C validator