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

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

Proof of Theorem eqimss
StepHypRef Expression
1 eqss 3112 . 2 (𝐴 = 𝐵 ↔ (𝐴𝐵𝐵𝐴))
21simplbi 272 1 (𝐴 = 𝐵𝐴𝐵)
Colors of variables: wff set class
Syntax hints:  wi 4   = wceq 1331  wss 3071
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121
This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084
This theorem is referenced by:  eqimss2  3152  uneqin  3327  sssnr  3680  sssnm  3681  ssprr  3683  sstpr  3684  snsspw  3691  pwpwssunieq  3901  elpwuni  3902  disjeq2  3910  disjeq1  3913  pwne  4084  pwssunim  4206  poeq2  4222  seeq1  4261  seeq2  4262  trsucss  4345  onsucelsucr  4424  xp11m  4977  funeq  5143  fnresdm  5232  fssxp  5290  ffdm  5293  fcoi1  5303  fof  5345  dff1o2  5372  fvmptss2  5496  fvmptssdm  5505  fprg  5603  dff1o6  5677  tposeq  6144  nntri1  6392  nntri2or2  6394  nnsseleq  6397  infnninf  7022  frec2uzf1od  10186  hashinfuni  10530  setsresg  12007  setsslid  12019  strle1g  12059  cncnpi  12407  hmeores  12494  limcimolemlt  12812  recnprss  12835  el2oss1o  13218  0nninf  13227  nninfall  13234
  Copyright terms: Public domain W3C validator