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

Theorem ssid 2992
Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Andrew Salmon, 14-Jun-2011.)
Assertion
Ref Expression
ssid  |-  A  C_  A

Proof of Theorem ssid
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 id 19 . 2  |-  ( x  e.  A  ->  x  e.  A )
21ssriv 2977 1  |-  A  C_  A
Colors of variables: wff set class
Syntax hints:    e. wcel 1409    C_ wss 2945
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-7 1353  ax-gen 1354  ax-ie1 1398  ax-ie2 1399  ax-8 1411  ax-11 1413  ax-4 1416  ax-17 1435  ax-i9 1439  ax-ial 1443  ax-i5r 1444  ax-ext 2038
This theorem depends on definitions:  df-bi 114  df-nf 1366  df-sb 1662  df-clab 2043  df-cleq 2049  df-clel 2052  df-in 2952  df-ss 2959
This theorem is referenced by:  eqimssi  3027  eqimss2i  3028  nsspssun  3198  inv1  3281  disjpss  3306  difid  3320  undifabs  3328  pwidg  3400  elssuni  3636  unimax  3642  intmin  3663  rintm  3772  iunpw  4239  sucprcreg  4301  tfisi  4338  peano5  4349  xpss1  4476  xpss2  4477  residm  4670  resdm  4677  resmpt3  4685  ssrnres  4791  dffn3  5081  fimacnv  5324  tfrlem1  5954  rdgss  6001  findcard2d  6379  findcard2sd  6380  1idprl  6746  1idpru  6747  ltexprlemm  6756  elq  8654  expcl  9438  iserclim0  10057
  Copyright terms: Public domain W3C validator