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

Theorem ssid 2964
 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 𝐴𝐴

Proof of Theorem ssid
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 id 19 . 2 (𝑥𝐴𝑥𝐴)
21ssriv 2949 1 𝐴𝐴
 Colors of variables: wff set class Syntax hints:   ∈ wcel 1393   ⊆ wss 2917 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-11 1397  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022 This theorem depends on definitions:  df-bi 110  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-in 2924  df-ss 2931 This theorem is referenced by:  eqimssi  2999  eqimss2i  3000  nsspssun  3170  inv1  3253  disjpss  3278  difid  3292  undifabs  3300  pwidg  3372  elssuni  3608  unimax  3614  intmin  3635  rintm  3744  iunpw  4211  sucprcreg  4273  tfisi  4310  peano5  4321  xpss1  4448  xpss2  4449  residm  4642  resdm  4649  resmpt3  4657  ssrnres  4763  dffn3  5053  fimacnv  5296  tfrlem1  5923  rdgss  5970  findcard2d  6348  findcard2sd  6349  1idprl  6688  1idpru  6689  ltexprlemm  6698  elq  8557  expcl  9273  iserclim0  9826
 Copyright terms: Public domain W3C validator