Theorem ssid 3117

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

Syntax hints:   e. wcel 1480   C_ wss 3071

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-in 3077  df-ss 3084

This theorem is referenced by:  ssidd  3118  eqimssi  3153  eqimss2i  3154  inv1  3399  difid  3431  undifabs  3439  pwidg  3524  elssuni  3764  unimax  3770  intmin  3791  rintm  3905  iunpw  4401  sucprcreg  4464  tfisi  4501  peano5  4512  xpss1  4649  xpss2  4650  residm  4851  resdm  4858  resmpt3  4868  ssrnres  4981  cocnvss  5064  dffn3  5283  fimacnv  5549  foima2  5653  tfrlem1  6205  rdgss  6280  fpmg  6568  findcard2d  6785  findcard2sd  6786  f1finf1o  6835  fidcenumlemr  6843  casef  6973  nnnninf  7023  1idprl  7398  1idpru  7399  ltexprlemm  7408  suplocexprlemmu  7526  elq  9414  expcl  10311  serclim0  11074  fsum2d  11204  fsumabs  11234  fsumiun  11246  reef11  11406  ressid  12020  topopn  12175  fiinbas  12216  topbas  12236  topcld  12278  ntrtop  12297  opnneissb  12324  opnssneib  12325  opnneiid  12333  idcn  12381  cnconst2  12402  lmres  12417  retopbas  12692  cnopncntop  12706  abscncf  12741  recncf  12742  imcncf  12743  cjcncf  12744  mulc1cncf  12745  cncfcn1cntop  12750  cncfmpt2fcntop  12754  addccncf  12755  cdivcncfap  12756  negfcncf  12758  expcncf  12761  cnrehmeocntop  12762  cnlimcim  12809  cnlimc  12810  cnlimci  12811  dvcnp2cntop  12832  dvcn  12833  dvef  12856  efcn  12857