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

Theorem eqimss2 3102
Description: Equality implies the subclass relation. (Contributed by NM, 23-Nov-2003.)
Assertion
Ref Expression
eqimss2 (𝐵 = 𝐴𝐴𝐵)

Proof of Theorem eqimss2
StepHypRef Expression
1 eqimss 3101 . 2 (𝐴 = 𝐵𝐴𝐵)
21eqcoms 2103 1 (𝐵 = 𝐴𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1299  wss 3021
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-11 1452  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082
This theorem depends on definitions:  df-bi 116  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-in 3027  df-ss 3034
This theorem is referenced by:  disjeq2  3856  disjeq1  3859  poeq2  4160  seeq1  4199  seeq2  4200  dmcoeq  4747  xp11m  4913  funeq  5079  fconst3m  5571  tposeq  6074  undifdcss  6740  ennnfonelemk  11705  ennnfonelemss  11715  qnnen  11736  topgele  11978  topontopn  11986  txdis  12227
  Copyright terms: Public domain W3C validator