Theorem ssid 3245

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

Syntax hints:   e. wcel 2200   C_ wss 3198

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3204  df-ss 3211

This theorem is referenced by:  ssidd  3246  eqimssi  3281  eqimss2i  3282  inv1  3529  difid  3561  undifabs  3569  pwidg  3664  elssuni  3919  unimax  3925  intmin  3946  rintm  4061  iunpw  4575  sucprcreg  4645  tfisi  4683  peano5  4694  xpss1  4834  xpss2  4835  residm  5043  resdm  5050  resmpt3  5060  ssrnres  5177  cocnvss  5260  dffn3  5490  fimacnv  5772  foima2  5887  tfrlem1  6469  rdgss  6544  fpmg  6838  findcard2d  7073  findcard2sd  7074  f1finf1o  7137  fidcenumlemr  7145  casef  7278  nnnninf  7316  1idprl  7800  1idpru  7801  ltexprlemm  7810  suplocexprlemmu  7928  elq  9846  expcl  10809  serclim0  11856  fsum2d  11986  fsumabs  12016  fsumiun  12028  fprod2d  12174  reef11  12250  ghmghmrn  13840  subrgid  14227  znf1o  14655  topopn  14722  fiinbas  14763  topbas  14781  topcld  14823  ntrtop  14842  opnneissb  14869  opnssneib  14870  opnneiid  14878  idcn  14926  cnconst2  14947  lmres  14962  retopbas  15237  cnopncntop  15258  cnopn  15259  abscncf  15299  recncf  15300  imcncf  15301  cjcncf  15302  mulc1cncf  15303  cncfcn1cntop  15308  cncfmpt2fcntop  15313  addccncf  15314  idcncf  15315  sub1cncf  15316  sub2cncf  15317  cdivcncfap  15318  negfcncf  15320  expcncf  15323  cnrehmeocntop  15324  maxcncf  15329  mincncf  15330  ivthreinc  15359  hovercncf  15360  cnlimcim  15385  cnlimc  15386  cnlimci  15387  dvcnp2cntop  15413  dvcn  15414  dvmptfsum  15439  dvef  15441  plyssc  15453  efcn  15482  domomsubct  16538