Theorem ssid 3177

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

Syntax hints:   e. wcel 2148   C_ wss 3131

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3137  df-ss 3144

This theorem is referenced by:  ssidd  3178  eqimssi  3213  eqimss2i  3214  inv1  3461  difid  3493  undifabs  3501  pwidg  3591  elssuni  3839  unimax  3845  intmin  3866  rintm  3981  iunpw  4482  sucprcreg  4550  tfisi  4588  peano5  4599  xpss1  4738  xpss2  4739  residm  4941  resdm  4948  resmpt3  4958  ssrnres  5073  cocnvss  5156  dffn3  5378  fimacnv  5647  foima2  5754  tfrlem1  6311  rdgss  6386  fpmg  6676  findcard2d  6893  findcard2sd  6894  f1finf1o  6948  fidcenumlemr  6956  casef  7089  nnnninf  7126  1idprl  7591  1idpru  7592  ltexprlemm  7601  suplocexprlemmu  7719  elq  9624  expcl  10540  serclim0  11315  fsum2d  11445  fsumabs  11475  fsumiun  11487  fprod2d  11633  reef11  11709  subrgid  13349  topopn  13547  fiinbas  13588  topbas  13606  topcld  13648  ntrtop  13667  opnneissb  13694  opnssneib  13695  opnneiid  13703  idcn  13751  cnconst2  13772  lmres  13787  retopbas  14062  cnopncntop  14076  abscncf  14111  recncf  14112  imcncf  14113  cjcncf  14114  mulc1cncf  14115  cncfcn1cntop  14120  cncfmpt2fcntop  14124  addccncf  14125  cdivcncfap  14126  negfcncf  14128  expcncf  14131  cnrehmeocntop  14132  cnlimcim  14179  cnlimc  14180  cnlimci  14181  dvcnp2cntop  14202  dvcn  14203  dvef  14227  efcn  14228