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  5892  tfrlem1  6474  rdgss  6549  fpmg  6843  findcard2d  7080  findcard2sd  7081  f1finf1o  7146  fidcenumlemr  7154  casef  7287  nnnninf  7325  1idprl  7810  1idpru  7811  ltexprlemm  7820  suplocexprlemmu  7938  elq  9856  expcl  10820  serclim0  11883  fsum2d  12014  fsumabs  12044  fsumiun  12056  fprod2d  12202  reef11  12278  ghmghmrn  13868  subrgid  14256  znf1o  14684  topopn  14751  fiinbas  14792  topbas  14810  topcld  14852  ntrtop  14871  opnneissb  14898  opnssneib  14899  opnneiid  14907  idcn  14955  cnconst2  14976  lmres  14991  retopbas  15266  cnopncntop  15287  cnopn  15288  abscncf  15328  recncf  15329  imcncf  15330  cjcncf  15331  mulc1cncf  15332  cncfcn1cntop  15337  cncfmpt2fcntop  15342  addccncf  15343  idcncf  15344  sub1cncf  15345  sub2cncf  15346  cdivcncfap  15347  negfcncf  15349  expcncf  15352  cnrehmeocntop  15353  maxcncf  15358  mincncf  15359  ivthreinc  15388  hovercncf  15389  cnlimcim  15414  cnlimc  15415  cnlimci  15416  dvcnp2cntop  15442  dvcn  15443  dvmptfsum  15468  dvef  15470  plyssc  15482  efcn  15511  uhgrsubgrself  16136  uhgrspansubgr  16147  domomsubct  16653