Theorem ssid 3244

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

Syntax hints:   e. wcel 2200   C_ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  ssidd  3245  eqimssi  3280  eqimss2i  3281  inv1  3528  difid  3560  undifabs  3568  pwidg  3663  elssuni  3916  unimax  3922  intmin  3943  rintm  4058  iunpw  4571  sucprcreg  4641  tfisi  4679  peano5  4690  xpss1  4829  xpss2  4830  residm  5037  resdm  5044  resmpt3  5054  ssrnres  5171  cocnvss  5254  dffn3  5484  fimacnv  5766  foima2  5881  tfrlem1  6460  rdgss  6535  fpmg  6829  findcard2d  7061  findcard2sd  7062  f1finf1o  7125  fidcenumlemr  7133  casef  7266  nnnninf  7304  1idprl  7788  1idpru  7789  ltexprlemm  7798  suplocexprlemmu  7916  elq  9829  expcl  10791  serclim0  11831  fsum2d  11961  fsumabs  11991  fsumiun  12003  fprod2d  12149  reef11  12225  ghmghmrn  13815  subrgid  14202  znf1o  14630  topopn  14697  fiinbas  14738  topbas  14756  topcld  14798  ntrtop  14817  opnneissb  14844  opnssneib  14845  opnneiid  14853  idcn  14901  cnconst2  14922  lmres  14937  retopbas  15212  cnopncntop  15233  cnopn  15234  abscncf  15274  recncf  15275  imcncf  15276  cjcncf  15277  mulc1cncf  15278  cncfcn1cntop  15283  cncfmpt2fcntop  15288  addccncf  15289  idcncf  15290  sub1cncf  15291  sub2cncf  15292  cdivcncfap  15293  negfcncf  15295  expcncf  15298  cnrehmeocntop  15299  maxcncf  15304  mincncf  15305  ivthreinc  15334  hovercncf  15335  cnlimcim  15360  cnlimc  15361  cnlimci  15362  dvcnp2cntop  15388  dvcn  15389  dvmptfsum  15414  dvef  15416  plyssc  15428  efcn  15457  domomsubct  16430