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

Theorem eqimss 3119
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  =  B  ->  A  C_  B )

Proof of Theorem eqimss
StepHypRef Expression
1 eqss 3080 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
21simplbi 270 1  |-  ( A  =  B  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1314    C_ wss 3039
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 1406  ax-7 1407  ax-gen 1408  ax-ie1 1452  ax-ie2 1453  ax-8 1465  ax-11 1467  ax-4 1470  ax-17 1489  ax-i9 1493  ax-ial 1497  ax-i5r 1498  ax-ext 2097
This theorem depends on definitions:  df-bi 116  df-nf 1420  df-sb 1719  df-clab 2102  df-cleq 2108  df-clel 2111  df-in 3045  df-ss 3052
This theorem is referenced by:  eqimss2  3120  uneqin  3295  sssnr  3648  sssnm  3649  ssprr  3651  sstpr  3652  snsspw  3659  pwpwssunieq  3869  elpwuni  3870  disjeq2  3878  disjeq1  3881  pwne  4052  pwssunim  4174  poeq2  4190  seeq1  4229  seeq2  4230  trsucss  4313  onsucelsucr  4392  xp11m  4945  funeq  5111  fnresdm  5200  fssxp  5258  ffdm  5261  fcoi1  5271  fof  5313  dff1o2  5338  fvmptss2  5462  fvmptssdm  5471  fprg  5569  dff1o6  5643  tposeq  6110  nntri1  6358  nntri2or2  6360  nnsseleq  6363  infnninf  6988  frec2uzf1od  10130  hashinfuni  10474  setsresg  11903  setsslid  11915  strle1g  11955  cncnpi  12303  hmeores  12390  limcimolemlt  12708  recnprss  12731  el2oss1o  13022  0nninf  13031  nninfall  13038
  Copyright terms: Public domain W3C validator