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  9303  elq  10022  expcl  10994  serclim0  12071  fsum2d  12202  fsumabs  12232  fsumiun  12244  fprod2d  12390  reef11  12466  ghmghmrn  14066  subrgid  14531  znf1o  14986  topopn  15109  fiinbas  15150  topbas  15168  topcld  15210  ntrtop  15229  opnneissb  15256  opnssneib  15257  opnneiid  15265  idcn  15313  cnconst2  15334  lmres  15349  retopbas  15624  cnopncntop  15645  cnopn  15646  abscncf  15686  recncf  15687  imcncf  15688  cjcncf  15689  mulc1cncf  15690  cncfcn1cntop  15695  cncfmpt2fcntop  15700  addccncf  15701  idcncf  15702  sub1cncf  15703  sub2cncf  15704  cdivcncfap  15705  negfcncf  15707  expcncf  15710  cnrehmeocntop  15711  maxcncf  15716  mincncf  15717  ivthreinc  15746  hovercncf  15747  cnlimcim  15772  cnlimc  15773  cnlimci  15774  dvcnp2cntop  15800  dvcn  15801  dvmptfsum  15826  dvef  15828  plyssc  15840  efcn  15869  uhgrsubgrself  16507  uhgrspansubgr  16518  domomsubct  17031