Theorem ssid 3221

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

Syntax hints:   e. wcel 2178   C_ wss 3174

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2189

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2194  df-cleq 2200  df-clel 2203  df-in 3180  df-ss 3187

This theorem is referenced by:  ssidd  3222  eqimssi  3257  eqimss2i  3258  inv1  3505  difid  3537  undifabs  3545  pwidg  3640  elssuni  3892  unimax  3898  intmin  3919  rintm  4034  iunpw  4545  sucprcreg  4615  tfisi  4653  peano5  4664  xpss1  4803  xpss2  4804  residm  5010  resdm  5017  resmpt3  5027  ssrnres  5144  cocnvss  5227  dffn3  5456  fimacnv  5732  foima2  5843  tfrlem1  6417  rdgss  6492  fpmg  6784  findcard2d  7014  findcard2sd  7015  f1finf1o  7075  fidcenumlemr  7083  casef  7216  nnnninf  7254  1idprl  7738  1idpru  7739  ltexprlemm  7748  suplocexprlemmu  7866  elq  9778  expcl  10739  serclim0  11731  fsum2d  11861  fsumabs  11891  fsumiun  11903  fprod2d  12049  reef11  12125  ghmghmrn  13714  subrgid  14100  znf1o  14528  topopn  14595  fiinbas  14636  topbas  14654  topcld  14696  ntrtop  14715  opnneissb  14742  opnssneib  14743  opnneiid  14751  idcn  14799  cnconst2  14820  lmres  14835  retopbas  15110  cnopncntop  15131  cnopn  15132  abscncf  15172  recncf  15173  imcncf  15174  cjcncf  15175  mulc1cncf  15176  cncfcn1cntop  15181  cncfmpt2fcntop  15186  addccncf  15187  idcncf  15188  sub1cncf  15189  sub2cncf  15190  cdivcncfap  15191  negfcncf  15193  expcncf  15196  cnrehmeocntop  15197  maxcncf  15202  mincncf  15203  ivthreinc  15232  hovercncf  15233  cnlimcim  15258  cnlimc  15259  cnlimci  15260  dvcnp2cntop  15286  dvcn  15287  dvmptfsum  15312  dvef  15314  plyssc  15326  efcn  15355  domomsubct  16140