Theorem ssid 3213

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

Syntax hints:   e. wcel 2176   C_ wss 3166

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 1470  ax-7 1471  ax-gen 1472  ax-ie1 1516  ax-ie2 1517  ax-8 1527  ax-11 1529  ax-4 1533  ax-17 1549  ax-i9 1553  ax-ial 1557  ax-i5r 1558  ax-ext 2187

This theorem depends on definitions:  df-bi 117  df-nf 1484  df-sb 1786  df-clab 2192  df-cleq 2198  df-clel 2201  df-in 3172  df-ss 3179

This theorem is referenced by:  ssidd  3214  eqimssi  3249  eqimss2i  3250  inv1  3497  difid  3529  undifabs  3537  pwidg  3630  elssuni  3878  unimax  3884  intmin  3905  rintm  4020  iunpw  4527  sucprcreg  4597  tfisi  4635  peano5  4646  xpss1  4785  xpss2  4786  residm  4991  resdm  4998  resmpt3  5008  ssrnres  5125  cocnvss  5208  dffn3  5436  fimacnv  5709  foima2  5820  tfrlem1  6394  rdgss  6469  fpmg  6761  findcard2d  6988  findcard2sd  6989  f1finf1o  7049  fidcenumlemr  7057  casef  7190  nnnninf  7228  1idprl  7703  1idpru  7704  ltexprlemm  7713  suplocexprlemmu  7831  elq  9743  expcl  10702  serclim0  11616  fsum2d  11746  fsumabs  11776  fsumiun  11788  fprod2d  11934  reef11  12010  ghmghmrn  13599  subrgid  13985  znf1o  14413  topopn  14480  fiinbas  14521  topbas  14539  topcld  14581  ntrtop  14600  opnneissb  14627  opnssneib  14628  opnneiid  14636  idcn  14684  cnconst2  14705  lmres  14720  retopbas  14995  cnopncntop  15016  cnopn  15017  abscncf  15057  recncf  15058  imcncf  15059  cjcncf  15060  mulc1cncf  15061  cncfcn1cntop  15066  cncfmpt2fcntop  15071  addccncf  15072  idcncf  15073  sub1cncf  15074  sub2cncf  15075  cdivcncfap  15076  negfcncf  15078  expcncf  15081  cnrehmeocntop  15082  maxcncf  15087  mincncf  15088  ivthreinc  15117  hovercncf  15118  cnlimcim  15143  cnlimc  15144  cnlimci  15145  dvcnp2cntop  15171  dvcn  15172  dvmptfsum  15197  dvef  15199  plyssc  15211  efcn  15240  domomsubct  15938