Theorem ssid 3247

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

Syntax hints:   e. wcel 2202   C_ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  ssidd  3248  eqimssi  3283  eqimss2i  3284  inv1  3531  difid  3563  undifabs  3571  pwidg  3666  elssuni  3921  unimax  3927  intmin  3948  rintm  4063  iunpw  4577  sucprcreg  4647  tfisi  4685  peano5  4696  xpss1  4836  xpss2  4837  residm  5045  resdm  5052  resmpt3  5062  ssrnres  5179  cocnvss  5262  dffn3  5493  fimacnv  5776  foima2  5891  tfrlem1  6473  rdgss  6548  fpmg  6842  findcard2d  7079  findcard2sd  7080  f1finf1o  7145  fidcenumlemr  7153  casef  7286  nnnninf  7324  1idprl  7809  1idpru  7810  ltexprlemm  7819  suplocexprlemmu  7937  elq  9855  expcl  10818  serclim0  11865  fsum2d  11995  fsumabs  12025  fsumiun  12037  fprod2d  12183  reef11  12259  ghmghmrn  13849  subrgid  14236  znf1o  14664  topopn  14731  fiinbas  14772  topbas  14790  topcld  14832  ntrtop  14851  opnneissb  14878  opnssneib  14879  opnneiid  14887  idcn  14935  cnconst2  14956  lmres  14971  retopbas  15246  cnopncntop  15267  cnopn  15268  abscncf  15308  recncf  15309  imcncf  15310  cjcncf  15311  mulc1cncf  15312  cncfcn1cntop  15317  cncfmpt2fcntop  15322  addccncf  15323  idcncf  15324  sub1cncf  15325  sub2cncf  15326  cdivcncfap  15327  negfcncf  15329  expcncf  15332  cnrehmeocntop  15333  maxcncf  15338  mincncf  15339  ivthreinc  15368  hovercncf  15369  cnlimcim  15394  cnlimc  15395  cnlimci  15396  dvcnp2cntop  15422  dvcn  15423  dvmptfsum  15448  dvef  15450  plyssc  15462  efcn  15491  uhgrsubgrself  16116  uhgrspansubgr  16127  domomsubct  16602