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  6583  rdgss  6658  fpmg  6959  findcard2d  7199  findcard2sd  7200  f1finf1o  7269  fidcenumlemr  7277  casef  7434  nnnninf  7472  1idprl  7963  1idpru  7964  ltexprlemm  7973  suplocexprlemmu  8091  indconst1  9312  elq  10038  expcl  11015  serclim0  12096  fsum2d  12227  fsumabs  12257  fsumiun  12269  fprod2d  12415  reef11  12491  ghmghmrn  14125  elcntr  14163  cntrnsg  14176  subrgid  14640  znf1o  15095  psrass1filem  15177  topopn  15234  fiinbas  15275  topbas  15293  topcld  15335  ntrtop  15354  opnneissb  15381  opnssneib  15382  opnneiid  15390  idcn  15438  cnconst2  15459  lmres  15474  retopbas  15749  cnopncntop  15770  cnopn  15771  abscncf  15811  recncf  15812  imcncf  15813  cjcncf  15814  mulc1cncf  15815  cncfcn1cntop  15820  cncfmpt2fcntop  15825  addccncf  15826  idcncf  15827  sub1cncf  15828  sub2cncf  15829  cdivcncfap  15830  negfcncf  15832  expcncf  15835  cnrehmeocntop  15836  maxcncf  15841  mincncf  15842  ivthreinc  15871  hovercncf  15872  cnlimcim  15897  cnlimc  15898  cnlimci  15899  dvcnp2cntop  15925  dvcn  15926  dvmptfsum  15951  dvef  15953  plyssc  15965  efcn  15994  uhgrsubgrself  16712  uhgrspansubgr  16723  domomsubct  17236