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

Theorem eqimss 3209
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 3170 . 2  |-  ( A  =  B  <->  ( A  C_  B  /\  B  C_  A ) )
21simplbi 274 1  |-  ( A  =  B  ->  A  C_  B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1353    C_ wss 3129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159
This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3135  df-ss 3142
This theorem is referenced by:  eqimss2  3210  uneqin  3386  sssnr  3751  sssnm  3752  ssprr  3754  sstpr  3755  snsspw  3762  pwpwssunieq  3972  elpwuni  3973  disjeq2  3981  disjeq1  3984  pwne  4157  pwssunim  4280  poeq2  4296  seeq1  4335  seeq2  4336  trsucss  4419  onsucelsucr  4503  xp11m  5062  funeq  5231  fnresdm  5320  fssxp  5378  ffdm  5381  fcoi1  5391  fof  5433  dff1o2  5461  fvmptss2  5586  fvmptssdm  5595  fprg  5694  dff1o6  5770  tposeq  6241  el2oss1o  6437  nntri1  6490  nntri2or2  6492  nnsseleq  6495  infnninf  7115  infnninfOLD  7116  nninfwlpoimlemg  7166  exmidontri2or  7235  frec2uzf1od  10379  hashinfuni  10728  setsresg  12470  setsslid  12482  strle1g  12533  cncnpi  13361  hmeores  13448  limcimolemlt  13766  recnprss  13789  0nninf  14376  nninfall  14381
  Copyright terms: Public domain W3C validator