Theorem ssid 3167

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

Syntax hints:   ∈ wcel 2141   ⊆ wss 3121

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 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-11 1499  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-ext 2152

This theorem depends on definitions:  df-bi 116  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-in 3127  df-ss 3134

This theorem is referenced by:  ssidd  3168  eqimssi  3203  eqimss2i  3204  inv1  3451  difid  3483  undifabs  3491  pwidg  3580  elssuni  3824  unimax  3830  intmin  3851  rintm  3965  iunpw  4465  sucprcreg  4533  tfisi  4571  peano5  4582  xpss1  4721  xpss2  4722  residm  4923  resdm  4930  resmpt3  4940  ssrnres  5053  cocnvss  5136  dffn3  5358  fimacnv  5625  foima2  5731  tfrlem1  6287  rdgss  6362  fpmg  6652  findcard2d  6869  findcard2sd  6870  f1finf1o  6924  fidcenumlemr  6932  casef  7065  nnnninf  7102  1idprl  7552  1idpru  7553  ltexprlemm  7562  suplocexprlemmu  7680  elq  9581  expcl  10494  serclim0  11268  fsum2d  11398  fsumabs  11428  fsumiun  11440  fprod2d  11586  reef11  11662  ressid  12479  topopn  12800  fiinbas  12841  topbas  12861  topcld  12903  ntrtop  12922  opnneissb  12949  opnssneib  12950  opnneiid  12958  idcn  13006  cnconst2  13027  lmres  13042  retopbas  13317  cnopncntop  13331  abscncf  13366  recncf  13367  imcncf  13368  cjcncf  13369  mulc1cncf  13370  cncfcn1cntop  13375  cncfmpt2fcntop  13379  addccncf  13380  cdivcncfap  13381  negfcncf  13383  expcncf  13386  cnrehmeocntop  13387  cnlimcim  13434  cnlimc  13435  cnlimci  13436  dvcnp2cntop  13457  dvcn  13458  dvef  13482  efcn  13483