Theorem ssid 3200

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

Syntax hints:   e. wcel 2164   C_ wss 3154

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-11 1517  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2175

This theorem depends on definitions:  df-bi 117  df-nf 1472  df-sb 1774  df-clab 2180  df-cleq 2186  df-clel 2189  df-in 3160  df-ss 3167

This theorem is referenced by:  ssidd  3201  eqimssi  3236  eqimss2i  3237  inv1  3484  difid  3516  undifabs  3524  pwidg  3616  elssuni  3864  unimax  3870  intmin  3891  rintm  4006  iunpw  4512  sucprcreg  4582  tfisi  4620  peano5  4631  xpss1  4770  xpss2  4771  residm  4975  resdm  4982  resmpt3  4992  ssrnres  5109  cocnvss  5192  dffn3  5415  fimacnv  5688  foima2  5795  tfrlem1  6363  rdgss  6438  fpmg  6730  findcard2d  6949  findcard2sd  6950  f1finf1o  7008  fidcenumlemr  7016  casef  7149  nnnninf  7187  1idprl  7652  1idpru  7653  ltexprlemm  7662  suplocexprlemmu  7780  elq  9690  expcl  10631  serclim0  11451  fsum2d  11581  fsumabs  11611  fsumiun  11623  fprod2d  11769  reef11  11845  ghmghmrn  13336  subrgid  13722  znf1o  14150  topopn  14187  fiinbas  14228  topbas  14246  topcld  14288  ntrtop  14307  opnneissb  14334  opnssneib  14335  opnneiid  14343  idcn  14391  cnconst2  14412  lmres  14427  retopbas  14702  cnopncntop  14723  cnopn  14724  abscncf  14764  recncf  14765  imcncf  14766  cjcncf  14767  mulc1cncf  14768  cncfcn1cntop  14773  cncfmpt2fcntop  14778  addccncf  14779  idcncf  14780  sub1cncf  14781  sub2cncf  14782  cdivcncfap  14783  negfcncf  14785  expcncf  14788  cnrehmeocntop  14789  maxcncf  14794  mincncf  14795  ivthreinc  14824  hovercncf  14825  cnlimcim  14850  cnlimc  14851  cnlimci  14852  dvcnp2cntop  14878  dvcn  14879  dvmptfsum  14904  dvef  14906  plyssc  14918  efcn  14944