Theorem ssid 3199

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

Syntax hints:   e. wcel 2164   C_ wss 3153

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3159  df-ss 3166

This theorem is referenced by:  ssidd  3200  eqimssi  3235  eqimss2i  3236  inv1  3483  difid  3515  undifabs  3523  pwidg  3615  elssuni  3863  unimax  3869  intmin  3890  rintm  4005  iunpw  4511  sucprcreg  4581  tfisi  4619  peano5  4630  xpss1  4769  xpss2  4770  residm  4974  resdm  4981  resmpt3  4991  ssrnres  5108  cocnvss  5191  dffn3  5414  fimacnv  5687  foima2  5794  tfrlem1  6361  rdgss  6436  fpmg  6728  findcard2d  6947  findcard2sd  6948  f1finf1o  7006  fidcenumlemr  7014  casef  7147  nnnninf  7185  1idprl  7650  1idpru  7651  ltexprlemm  7660  suplocexprlemmu  7778  elq  9687  expcl  10628  serclim0  11448  fsum2d  11578  fsumabs  11608  fsumiun  11620  fprod2d  11766  reef11  11842  ghmghmrn  13333  subrgid  13719  znf1o  14139  topopn  14176  fiinbas  14217  topbas  14235  topcld  14277  ntrtop  14296  opnneissb  14323  opnssneib  14324  opnneiid  14332  idcn  14380  cnconst2  14401  lmres  14416  retopbas  14691  cnopncntop  14705  abscncf  14740  recncf  14741  imcncf  14742  cjcncf  14743  mulc1cncf  14744  cncfcn1cntop  14749  cncfmpt2fcntop  14753  addccncf  14754  idcncf  14755  sub1cncf  14756  sub2cncf  14757  cdivcncfap  14758  negfcncf  14760  expcncf  14763  cnrehmeocntop  14764  maxcncf  14769  mincncf  14770  ivthreinc  14799  hovercncf  14800  cnlimcim  14825  cnlimc  14826  cnlimci  14827  dvcnp2cntop  14848  dvcn  14849  dvef  14873  plyssc  14885  efcn  14903