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

This proof depends on syntax axioms:   e. wcel 2209   C_ wss 3220

This proof depends on 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 proof 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 used by:  ssidd  3269  eqimssi  3304  eqimss2i  3305  inv1  3559  difid  3594  disjdif  3599  undifabs  3604  pwidg  3706  elssuni  3963  unimax  3969  intmin  3990  rintm  4105  iunpw  4626  sucprcreg  4696  tfisi  4734  peano5  4745  xpss1  4885  xpss2  4886  residm  5095  resdm  5102  resmpt3  5112  ssrnres  5230  cocnvss  5313  dffn3  5544  fimacnv  5837  foima2  5957  fdmrn  6034  tfrlem1  6579  rdgss  6654  fpmg  6955  findcard2d  7195  findcard2sd  7196  f1finf1o  7264  fidcenumlemr  7272  casef  7428  nnnninf  7466  1idprl  7957  1idpru  7958  ltexprlemm  7967  suplocexprlemmu  8085  indconst1  9305  elq  10031  expcl  11007  serclim0  12087  fsum2d  12218  fsumabs  12248  fsumiun  12260  fprod2d  12406  reef11  12482  ghmghmrn  14115  subrgid  14580  znf1o  15035  topopn  15158  fiinbas  15199  topbas  15217  topcld  15259  ntrtop  15278  opnneissb  15305  opnssneib  15306  opnneiid  15314  idcn  15362  cnconst2  15383  lmres  15398  retopbas  15673  cnopncntop  15694  cnopn  15695  abscncf  15735  recncf  15736  imcncf  15737  cjcncf  15738  mulc1cncf  15739  cncfcn1cntop  15744  cncfmpt2fcntop  15749  addccncf  15750  idcncf  15751  sub1cncf  15752  sub2cncf  15753  cdivcncfap  15754  negfcncf  15756  expcncf  15759  cnrehmeocntop  15760  maxcncf  15765  mincncf  15766  ivthreinc  15795  hovercncf  15796  cnlimcim  15821  cnlimc  15822  cnlimci  15823  dvcnp2cntop  15849  dvcn  15850  dvmptfsum  15875  dvef  15877  plyssc  15889  efcn  15918  uhgrsubgrself  16605  uhgrspansubgr  16616  domomsubct  17129