Theorem ssid 3173

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

Syntax hints:   e. wcel 2146   C_ wss 3127

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 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-11 1504  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157

This theorem depends on definitions:  df-bi 117  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-in 3133  df-ss 3140

This theorem is referenced by:  ssidd  3174  eqimssi  3209  eqimss2i  3210  inv1  3457  difid  3489  undifabs  3497  pwidg  3586  elssuni  3833  unimax  3839  intmin  3860  rintm  3974  iunpw  4474  sucprcreg  4542  tfisi  4580  peano5  4591  xpss1  4730  xpss2  4731  residm  4932  resdm  4939  resmpt3  4949  ssrnres  5063  cocnvss  5146  dffn3  5368  fimacnv  5637  foima2  5743  tfrlem1  6299  rdgss  6374  fpmg  6664  findcard2d  6881  findcard2sd  6882  f1finf1o  6936  fidcenumlemr  6944  casef  7077  nnnninf  7114  1idprl  7564  1idpru  7565  ltexprlemm  7574  suplocexprlemmu  7692  elq  9595  expcl  10508  serclim0  11281  fsum2d  11411  fsumabs  11441  fsumiun  11453  fprod2d  11599  reef11  11675  ressid  12492  topopn  13077  fiinbas  13118  topbas  13138  topcld  13180  ntrtop  13199  opnneissb  13226  opnssneib  13227  opnneiid  13235  idcn  13283  cnconst2  13304  lmres  13319  retopbas  13594  cnopncntop  13608  abscncf  13643  recncf  13644  imcncf  13645  cjcncf  13646  mulc1cncf  13647  cncfcn1cntop  13652  cncfmpt2fcntop  13656  addccncf  13657  cdivcncfap  13658  negfcncf  13660  expcncf  13663  cnrehmeocntop  13664  cnlimcim  13711  cnlimc  13712  cnlimci  13713  dvcnp2cntop  13734  dvcn  13735  dvef  13759  efcn  13760