Theorem ssid 3081

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

Syntax hints:   e. wcel 1461   C_ wss 3035

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1404  ax-7 1405  ax-gen 1406  ax-ie1 1450  ax-ie2 1451  ax-8 1463  ax-11 1465  ax-4 1468  ax-17 1487  ax-i9 1491  ax-ial 1495  ax-i5r 1496  ax-ext 2095

This theorem depends on definitions:  df-bi 116  df-nf 1418  df-sb 1717  df-clab 2100  df-cleq 2106  df-clel 2109  df-in 3041  df-ss 3048

This theorem is referenced by:  ssidd  3082  eqimssi  3117  eqimss2i  3118  inv1  3363  difid  3395  undifabs  3403  pwidg  3488  elssuni  3728  unimax  3734  intmin  3755  rintm  3869  iunpw  4359  sucprcreg  4422  tfisi  4459  peano5  4470  xpss1  4607  xpss2  4608  residm  4807  resdm  4814  resmpt3  4824  ssrnres  4937  cocnvss  5020  dffn3  5239  fimacnv  5501  foima2  5605  tfrlem1  6157  rdgss  6232  fpmg  6520  findcard2d  6736  findcard2sd  6737  f1finf1o  6785  fidcenumlemr  6793  casef  6923  nnnninf  6971  1idprl  7340  1idpru  7341  ltexprlemm  7350  elq  9310  expcl  10198  serclim0  10960  fsum2d  11090  fsumabs  11120  fsumiun  11132  reef11  11251  ressid  11857  topopn  12012  fiinbas  12053  topbas  12073  topcld  12115  ntrtop  12134  opnneissb  12161  opnssneib  12162  opnneiid  12170  idcn  12217  cnconst2  12238  lmres  12253  retopbas  12506  abscncf  12552  recncf  12553  imcncf  12554  cjcncf  12555  mulc1cncf  12556  cncfcn1cntop  12561  cncfmpt2fcntop  12565  addccncf  12566  cdivcncfap  12567  negfcncf  12569  expcncf  12572  cnlimcim  12590  cnlimc  12591  cnlimci  12592  dvcnp2cntop  12612  dvcn  12613