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  7429  nnnninf  7467  1idprl  7958  1idpru  7959  ltexprlemm  7968  suplocexprlemmu  8086  indconst1  9306  elq  10032  expcl  11009  serclim0  12090  fsum2d  12221  fsumabs  12251  fsumiun  12263  fprod2d  12409  reef11  12485  ghmghmrn  14119  elcntr  14157  cntrnsg  14170  subrgid  14615  znf1o  15070  topopn  15200  fiinbas  15241  topbas  15259  topcld  15301  ntrtop  15320  opnneissb  15347  opnssneib  15348  opnneiid  15356  idcn  15404  cnconst2  15425  lmres  15440  retopbas  15715  cnopncntop  15736  cnopn  15737  abscncf  15777  recncf  15778  imcncf  15779  cjcncf  15780  mulc1cncf  15781  cncfcn1cntop  15786  cncfmpt2fcntop  15791  addccncf  15792  idcncf  15793  sub1cncf  15794  sub2cncf  15795  cdivcncfap  15796  negfcncf  15798  expcncf  15801  cnrehmeocntop  15802  maxcncf  15807  mincncf  15808  ivthreinc  15837  hovercncf  15838  cnlimcim  15863  cnlimc  15864  cnlimci  15865  dvcnp2cntop  15891  dvcn  15892  dvmptfsum  15917  dvef  15919  plyssc  15931  efcn  15960  uhgrsubgrself  16673  uhgrspansubgr  16684  domomsubct  17197