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  4628  sucprcreg  4698  tfisi  4736  peano5  4747  xpss1  4887  xpss2  4888  residm  5097  resdm  5104  resmpt3  5115  ssrnres  5233  cocnvss  5316  dffn3  5547  fimacnv  5840  foima2  5960  fdmrn  6037  tfrlem1  6584  rdgss  6659  fpmg  6960  findcard2d  7201  findcard2sd  7202  f1finf1o  7271  fidcenumlemr  7279  snopfsupp  7306  casef  7434  nnnninf  7472  1idprl  7963  1idpru  7964  ltexprlemm  7973  suplocexprlemmu  8091  indconst1  9312  elq  10037  expcl  11014  serclim0  12095  fsum2d  12226  fsumabs  12256  fsumiun  12268  fprod2d  12414  reef11  12490  ghmghmrn  14124  elcntr  14162  cntrnsg  14175  subrgid  14639  znf1o  15094  psrass1filem  15186  topopn  15251  fiinbas  15292  topbas  15310  topcld  15352  ntrtop  15371  opnneissb  15398  opnssneib  15399  opnneiid  15407  idcn  15455  cnconst2  15476  lmres  15491  retopbas  15766  cnopncntop  15787  cnopn  15788  abscncf  15828  recncf  15829  imcncf  15830  cjcncf  15831  mulc1cncf  15832  cncfcn1cntop  15837  cncfmpt2fcntop  15842  addccncf  15843  idcncf  15844  sub1cncf  15845  sub2cncf  15846  cdivcncfap  15847  negfcncf  15849  expcncf  15852  cnrehmeocntop  15853  maxcncf  15858  mincncf  15859  ivthreinc  15888  hovercncf  15889  cnlimcim  15914  cnlimc  15915  cnlimci  15916  dvcnp2cntop  15942  dvcn  15943  dvmptfsum  15968  dvef  15970  plyssc  15982  efcn  16011  uhgrsubgrself  16729  uhgrspansubgr  16740  domomsubct  17253