Theorem ssid 3244

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

Syntax hints:   e. wcel 2200   C_ wss 3197

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 3203  df-ss 3210

This theorem is referenced by:  ssidd  3245  eqimssi  3280  eqimss2i  3281  inv1  3528  difid  3560  undifabs  3568  pwidg  3663  elssuni  3915  unimax  3921  intmin  3942  rintm  4057  iunpw  4570  sucprcreg  4640  tfisi  4678  peano5  4689  xpss1  4828  xpss2  4829  residm  5036  resdm  5043  resmpt3  5053  ssrnres  5170  cocnvss  5253  dffn3  5483  fimacnv  5763  foima2  5874  tfrlem1  6452  rdgss  6527  fpmg  6819  findcard2d  7049  findcard2sd  7050  f1finf1o  7110  fidcenumlemr  7118  casef  7251  nnnninf  7289  1idprl  7773  1idpru  7774  ltexprlemm  7783  suplocexprlemmu  7901  elq  9813  expcl  10774  serclim0  11811  fsum2d  11941  fsumabs  11971  fsumiun  11983  fprod2d  12129  reef11  12205  ghmghmrn  13795  subrgid  14181  znf1o  14609  topopn  14676  fiinbas  14717  topbas  14735  topcld  14777  ntrtop  14796  opnneissb  14823  opnssneib  14824  opnneiid  14832  idcn  14880  cnconst2  14901  lmres  14916  retopbas  15191  cnopncntop  15212  cnopn  15213  abscncf  15253  recncf  15254  imcncf  15255  cjcncf  15256  mulc1cncf  15257  cncfcn1cntop  15262  cncfmpt2fcntop  15267  addccncf  15268  idcncf  15269  sub1cncf  15270  sub2cncf  15271  cdivcncfap  15272  negfcncf  15274  expcncf  15277  cnrehmeocntop  15278  maxcncf  15283  mincncf  15284  ivthreinc  15313  hovercncf  15314  cnlimcim  15339  cnlimc  15340  cnlimci  15341  dvcnp2cntop  15367  dvcn  15368  dvmptfsum  15393  dvef  15395  plyssc  15407  efcn  15436  domomsubct  16326