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	|- A C_ A

Proof of Theorem ssid

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( x e. A -> x e. A )
2	1	ssriv 2949	1 |- A C_ A

Syntax hints:   e. wcel 1393   C_ 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