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

Theorem eqssd 3031
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 3029 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
41, 2, 3sylanbrc 408 1 (𝜑𝐴 = 𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1287  wss 2988
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 2994  df-ss 3001
This theorem is referenced by:  eqrd  3032  unissel  3665  intmin  3691  int0el  3701  exmidundif  4009  dmcosseq  4672  relfld  4925  imadif  5059  imain  5061  fimacnv  5391  fo2ndf  5949  tposeq  5966  tfrlemibfn  6047  tfrlemi14d  6052  tfr1onlembfn  6063  tfri1dALT  6070  tfrcllembfn  6076  dcdifsnid  6217  fisbth  6551  en2eqpr  6575  exmidpw  6576  undifdcss  6585  en2other2  6766  addnqpr  7064  mulnqpr  7080  distrprg  7091  ltexpri  7116  addcanprg  7119  recexprlemex  7140  aptipr  7144  cauappcvgprlemladd  7161  fzopth  9406  fzosplit  9516  fzouzsplit  9518  frecuzrdgtcl  9747  frecuzrdgdomlem  9752  phimullem  11076  findset  11278
  Copyright terms: Public domain W3C validator