Theorem ssid 3248

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 3232	1 |- A C_ A

Syntax hints:   e. wcel 2202   C_ wss 3201

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  ssidd  3249  eqimssi  3284  eqimss2i  3285  inv1  3533  difid  3565  undifabs  3573  pwidg  3670  elssuni  3926  unimax  3932  intmin  3953  rintm  4068  iunpw  4583  sucprcreg  4653  tfisi  4691  peano5  4702  xpss1  4842  xpss2  4843  residm  5051  resdm  5058  resmpt3  5068  ssrnres  5186  cocnvss  5269  dffn3  5500  fimacnv  5784  foima2  5902  tfrlem1  6517  rdgss  6592  fpmg  6886  findcard2d  7123  findcard2sd  7124  f1finf1o  7189  fidcenumlemr  7197  casef  7330  nnnninf  7368  1idprl  7853  1idpru  7854  ltexprlemm  7863  suplocexprlemmu  7981  elq  9900  expcl  10865  serclim0  11928  fsum2d  12059  fsumabs  12089  fsumiun  12101  fprod2d  12247  reef11  12323  ghmghmrn  13913  subrgid  14301  znf1o  14730  topopn  14802  fiinbas  14843  topbas  14861  topcld  14903  ntrtop  14922  opnneissb  14949  opnssneib  14950  opnneiid  14958  idcn  15006  cnconst2  15027  lmres  15042  retopbas  15317  cnopncntop  15338  cnopn  15339  abscncf  15379  recncf  15380  imcncf  15381  cjcncf  15382  mulc1cncf  15383  cncfcn1cntop  15388  cncfmpt2fcntop  15393  addccncf  15394  idcncf  15395  sub1cncf  15396  sub2cncf  15397  cdivcncfap  15398  negfcncf  15400  expcncf  15403  cnrehmeocntop  15404  maxcncf  15409  mincncf  15410  ivthreinc  15439  hovercncf  15440  cnlimcim  15465  cnlimc  15466  cnlimci  15467  dvcnp2cntop  15493  dvcn  15494  dvmptfsum  15519  dvef  15521  plyssc  15533  efcn  15562  uhgrsubgrself  16190  uhgrspansubgr  16201  domomsubct  16706