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

Theorem eqimss 2973
Description: Equality implies the subclass relation. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 21-Jun-2011.)
Assertion
Ref Expression
eqimss (A = BAB)

Proof of Theorem eqimss
StepHypRef Expression
1 eqss 2936 . 2 (A = B ↔ (AB BA))
21simplbi 259 1 (A = BAB)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1228  wss 2893
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 1364  ax-ie2 1365  ax-8 1377  ax-11 1379  ax-4 1382  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2005
This theorem depends on definitions:  df-bi 110  df-nf 1330  df-sb 1629  df-clab 2010  df-cleq 2016  df-clel 2019  df-in 2900  df-ss 2907
This theorem is referenced by:  eqimss2  2974  sspssr  3019  sspsstrir  3022  uneqin  3164  sssnr  3497  sssnm  3498  ssprr  3500  sstpr  3501  snsspw  3508  elpwuni  3714  disjeq2  3722  disjeq1  3725  pwne  3886  pwssunim  3994  poeq2  4010  seeq1  4042  seeq2  4043  trsucss  4108  onsucelsucr  4181  xp11m  4684  funeq  4845  fnresdm  4932  fssxp  4981  ffdm  4984  fcoi1  4993  fof  5029  dff1o2  5054  fvmptss2  5170  fvmptssdm  5178  fprg  5269  dff1o6  5339  tposeq  5781  nntri1  5984
  Copyright terms: Public domain W3C validator