Theorem ssid 3204

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

Syntax hints:   e. wcel 2167   C_ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  ssidd  3205  eqimssi  3240  eqimss2i  3241  inv1  3488  difid  3520  undifabs  3528  pwidg  3620  elssuni  3868  unimax  3874  intmin  3895  rintm  4010  iunpw  4516  sucprcreg  4586  tfisi  4624  peano5  4635  xpss1  4774  xpss2  4775  residm  4979  resdm  4986  resmpt3  4996  ssrnres  5113  cocnvss  5196  dffn3  5421  fimacnv  5694  foima2  5801  tfrlem1  6375  rdgss  6450  fpmg  6742  findcard2d  6961  findcard2sd  6962  f1finf1o  7022  fidcenumlemr  7030  casef  7163  nnnninf  7201  1idprl  7674  1idpru  7675  ltexprlemm  7684  suplocexprlemmu  7802  elq  9713  expcl  10666  serclim0  11487  fsum2d  11617  fsumabs  11647  fsumiun  11659  fprod2d  11805  reef11  11881  ghmghmrn  13469  subrgid  13855  znf1o  14283  topopn  14328  fiinbas  14369  topbas  14387  topcld  14429  ntrtop  14448  opnneissb  14475  opnssneib  14476  opnneiid  14484  idcn  14532  cnconst2  14553  lmres  14568  retopbas  14843  cnopncntop  14864  cnopn  14865  abscncf  14905  recncf  14906  imcncf  14907  cjcncf  14908  mulc1cncf  14909  cncfcn1cntop  14914  cncfmpt2fcntop  14919  addccncf  14920  idcncf  14921  sub1cncf  14922  sub2cncf  14923  cdivcncfap  14924  negfcncf  14926  expcncf  14929  cnrehmeocntop  14930  maxcncf  14935  mincncf  14936  ivthreinc  14965  hovercncf  14966  cnlimcim  14991  cnlimc  14992  cnlimci  14993  dvcnp2cntop  15019  dvcn  15020  dvmptfsum  15045  dvef  15047  plyssc  15059  efcn  15088  domomsubct  15732