Theorem ssid 3162

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

Syntax hints:   ∈ wcel 2136   ⊆ wss 3116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1435  ax-7 1436  ax-gen 1437  ax-ie1 1481  ax-ie2 1482  ax-8 1492  ax-11 1494  ax-4 1498  ax-17 1514  ax-i9 1518  ax-ial 1522  ax-i5r 1523  ax-ext 2147

This theorem depends on definitions:  df-bi 116  df-nf 1449  df-sb 1751  df-clab 2152  df-cleq 2158  df-clel 2161  df-in 3122  df-ss 3129

This theorem is referenced by:  ssidd  3163  eqimssi  3198  eqimss2i  3199  inv1  3445  difid  3477  undifabs  3485  pwidg  3573  elssuni  3817  unimax  3823  intmin  3844  rintm  3958  iunpw  4458  sucprcreg  4526  tfisi  4564  peano5  4575  xpss1  4714  xpss2  4715  residm  4916  resdm  4923  resmpt3  4933  ssrnres  5046  cocnvss  5129  dffn3  5348  fimacnv  5614  foima2  5720  tfrlem1  6276  rdgss  6351  fpmg  6640  findcard2d  6857  findcard2sd  6858  f1finf1o  6912  fidcenumlemr  6920  casef  7053  nnnninf  7090  1idprl  7531  1idpru  7532  ltexprlemm  7541  suplocexprlemmu  7659  elq  9560  expcl  10473  serclim0  11246  fsum2d  11376  fsumabs  11406  fsumiun  11418  fprod2d  11564  reef11  11640  ressid  12456  topopn  12646  fiinbas  12687  topbas  12707  topcld  12749  ntrtop  12768  opnneissb  12795  opnssneib  12796  opnneiid  12804  idcn  12852  cnconst2  12873  lmres  12888  retopbas  13163  cnopncntop  13177  abscncf  13212  recncf  13213  imcncf  13214  cjcncf  13215  mulc1cncf  13216  cncfcn1cntop  13221  cncfmpt2fcntop  13225  addccncf  13226  cdivcncfap  13227  negfcncf  13229  expcncf  13232  cnrehmeocntop  13233  cnlimcim  13280  cnlimc  13281  cnlimci  13282  dvcnp2cntop  13303  dvcn  13304  dvef  13328  efcn  13329