Theorem ssid 3245

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	⊢ 𝐴 ⊆ 𝐴

Proof of Theorem ssid

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝐴)
2	1	ssriv 3229	1 ⊢ 𝐴 ⊆ 𝐴

Syntax hints:   ∈ wcel 2200   ⊆ wss 3198

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 3204  df-ss 3211

This theorem is referenced by:  ssidd  3246  eqimssi  3281  eqimss2i  3282  inv1  3529  difid  3561  undifabs  3569  pwidg  3664  elssuni  3919  unimax  3925  intmin  3946  rintm  4061  iunpw  4575  sucprcreg  4645  tfisi  4683  peano5  4694  xpss1  4834  xpss2  4835  residm  5043  resdm  5050  resmpt3  5060  ssrnres  5177  cocnvss  5260  dffn3  5490  fimacnv  5772  foima2  5887  tfrlem1  6469  rdgss  6544  fpmg  6838  findcard2d  7075  findcard2sd  7076  f1finf1o  7140  fidcenumlemr  7148  casef  7281  nnnninf  7319  1idprl  7803  1idpru  7804  ltexprlemm  7813  suplocexprlemmu  7931  elq  9849  expcl  10812  serclim0  11859  fsum2d  11989  fsumabs  12019  fsumiun  12031  fprod2d  12177  reef11  12253  ghmghmrn  13843  subrgid  14230  znf1o  14658  topopn  14725  fiinbas  14766  topbas  14784  topcld  14826  ntrtop  14845  opnneissb  14872  opnssneib  14873  opnneiid  14881  idcn  14929  cnconst2  14950  lmres  14965  retopbas  15240  cnopncntop  15261  cnopn  15262  abscncf  15302  recncf  15303  imcncf  15304  cjcncf  15305  mulc1cncf  15306  cncfcn1cntop  15311  cncfmpt2fcntop  15316  addccncf  15317  idcncf  15318  sub1cncf  15319  sub2cncf  15320  cdivcncfap  15321  negfcncf  15323  expcncf  15326  cnrehmeocntop  15327  maxcncf  15332  mincncf  15333  ivthreinc  15362  hovercncf  15363  cnlimcim  15388  cnlimc  15389  cnlimci  15390  dvcnp2cntop  15416  dvcn  15417  dvmptfsum  15442  dvef  15444  plyssc  15456  efcn  15485  domomsubct  16552