Theorem ssid 3258

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

Syntax hints:   e. wcel 2203   C_ wss 3211

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 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3217  df-ss 3224

This theorem is referenced by:  ssidd  3259  eqimssi  3294  eqimss2i  3295  inv1  3545  difid  3577  undifabs  3586  pwidg  3686  elssuni  3942  unimax  3948  intmin  3969  rintm  4084  iunpw  4601  sucprcreg  4671  tfisi  4709  peano5  4720  xpss1  4860  xpss2  4861  residm  5070  resdm  5077  resmpt3  5087  ssrnres  5205  cocnvss  5288  dffn3  5519  fimacnv  5806  foima2  5924  tfrlem1  6539  rdgss  6614  fpmg  6908  findcard2d  7148  findcard2sd  7149  f1finf1o  7217  fidcenumlemr  7225  casef  7379  nnnninf  7417  1idprl  7905  1idpru  7906  ltexprlemm  7915  suplocexprlemmu  8033  elq  9954  expcl  10919  serclim0  11990  fsum2d  12121  fsumabs  12151  fsumiun  12163  fprod2d  12309  reef11  12385  ghmghmrn  13980  subrgid  14368  znf1o  14799  topopn  14873  fiinbas  14914  topbas  14932  topcld  14974  ntrtop  14993  opnneissb  15020  opnssneib  15021  opnneiid  15029  idcn  15077  cnconst2  15098  lmres  15113  retopbas  15388  cnopncntop  15409  cnopn  15410  abscncf  15450  recncf  15451  imcncf  15452  cjcncf  15453  mulc1cncf  15454  cncfcn1cntop  15459  cncfmpt2fcntop  15464  addccncf  15465  idcncf  15466  sub1cncf  15467  sub2cncf  15468  cdivcncfap  15469  negfcncf  15471  expcncf  15474  cnrehmeocntop  15475  maxcncf  15480  mincncf  15481  ivthreinc  15510  hovercncf  15511  cnlimcim  15536  cnlimc  15537  cnlimci  15538  dvcnp2cntop  15564  dvcn  15565  dvmptfsum  15590  dvef  15592  plyssc  15604  efcn  15633  uhgrsubgrself  16261  uhgrspansubgr  16272  domomsubct  16775