Theorem ssid 3268

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

Syntax hints:   e. wcel 2209   C_ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  ssidd  3269  eqimssi  3304  eqimss2i  3305  inv1  3559  difid  3592  undifabs  3601  pwidg  3702  elssuni  3958  unimax  3964  intmin  3985  rintm  4100  iunpw  4621  sucprcreg  4691  tfisi  4729  peano5  4740  xpss1  4880  xpss2  4881  residm  5090  resdm  5097  resmpt3  5107  ssrnres  5225  cocnvss  5308  dffn3  5539  fimacnv  5828  foima2  5947  fdmrn  6024  tfrlem1  6569  rdgss  6644  fpmg  6945  findcard2d  7185  findcard2sd  7186  f1finf1o  7254  fidcenumlemr  7262  casef  7418  nnnninf  7456  1idprl  7947  1idpru  7948  ltexprlemm  7957  suplocexprlemmu  8075  elq  10001  expcl  10972  serclim0  12049  fsum2d  12180  fsumabs  12210  fsumiun  12222  fprod2d  12368  reef11  12444  ghmghmrn  14043  subrgid  14504  znf1o  14958  topopn  15032  fiinbas  15073  topbas  15091  topcld  15133  ntrtop  15152  opnneissb  15179  opnssneib  15180  opnneiid  15188  idcn  15236  cnconst2  15257  lmres  15272  retopbas  15547  cnopncntop  15568  cnopn  15569  abscncf  15609  recncf  15610  imcncf  15611  cjcncf  15612  mulc1cncf  15613  cncfcn1cntop  15618  cncfmpt2fcntop  15623  addccncf  15624  idcncf  15625  sub1cncf  15626  sub2cncf  15627  cdivcncfap  15628  negfcncf  15630  expcncf  15633  cnrehmeocntop  15634  maxcncf  15639  mincncf  15640  ivthreinc  15669  hovercncf  15670  cnlimcim  15695  cnlimc  15696  cnlimci  15697  dvcnp2cntop  15723  dvcn  15724  dvmptfsum  15749  dvef  15751  plyssc  15763  efcn  15792  uhgrsubgrself  16421  uhgrspansubgr  16432  domomsubct  16945