Theorem ssid 3262

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

Syntax hints:   e. wcel 2205   C_ wss 3214

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  ssidd  3263  eqimssi  3298  eqimss2i  3299  inv1  3549  difid  3581  undifabs  3590  pwidg  3691  elssuni  3947  unimax  3953  intmin  3974  rintm  4089  iunpw  4606  sucprcreg  4676  tfisi  4714  peano5  4725  xpss1  4865  xpss2  4866  residm  5075  resdm  5082  resmpt3  5092  ssrnres  5210  cocnvss  5293  dffn3  5524  fimacnv  5811  foima2  5930  fdmrn  6007  tfrlem1  6552  rdgss  6627  fpmg  6921  findcard2d  7161  findcard2sd  7162  f1finf1o  7230  fidcenumlemr  7238  casef  7392  nnnninf  7430  1idprl  7921  1idpru  7922  ltexprlemm  7931  suplocexprlemmu  8049  elq  9972  expcl  10943  serclim0  12015  fsum2d  12146  fsumabs  12176  fsumiun  12188  fprod2d  12334  reef11  12410  ghmghmrn  14016  subrgid  14469  znf1o  14925  topopn  14999  fiinbas  15040  topbas  15058  topcld  15100  ntrtop  15119  opnneissb  15146  opnssneib  15147  opnneiid  15155  idcn  15203  cnconst2  15224  lmres  15239  retopbas  15514  cnopncntop  15535  cnopn  15536  abscncf  15576  recncf  15577  imcncf  15578  cjcncf  15579  mulc1cncf  15580  cncfcn1cntop  15585  cncfmpt2fcntop  15590  addccncf  15591  idcncf  15592  sub1cncf  15593  sub2cncf  15594  cdivcncfap  15595  negfcncf  15597  expcncf  15600  cnrehmeocntop  15601  maxcncf  15606  mincncf  15607  ivthreinc  15636  hovercncf  15637  cnlimcim  15662  cnlimc  15663  cnlimci  15664  dvcnp2cntop  15690  dvcn  15691  dvmptfsum  15716  dvef  15718  plyssc  15730  efcn  15759  uhgrsubgrself  16387  uhgrspansubgr  16398  domomsubct  16901