Theorem ssid 3203

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

Syntax hints:   ∈ wcel 2167   ⊆ wss 3157

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 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-11 1520  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178

This theorem depends on definitions:  df-bi 117  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-in 3163  df-ss 3170

This theorem is referenced by:  ssidd  3204  eqimssi  3239  eqimss2i  3240  inv1  3487  difid  3519  undifabs  3527  pwidg  3619  elssuni  3867  unimax  3873  intmin  3894  rintm  4009  iunpw  4515  sucprcreg  4585  tfisi  4623  peano5  4634  xpss1  4773  xpss2  4774  residm  4978  resdm  4985  resmpt3  4995  ssrnres  5112  cocnvss  5195  dffn3  5418  fimacnv  5691  foima2  5798  tfrlem1  6366  rdgss  6441  fpmg  6733  findcard2d  6952  findcard2sd  6953  f1finf1o  7013  fidcenumlemr  7021  casef  7154  nnnninf  7192  1idprl  7657  1idpru  7658  ltexprlemm  7667  suplocexprlemmu  7785  elq  9696  expcl  10649  serclim0  11470  fsum2d  11600  fsumabs  11630  fsumiun  11642  fprod2d  11788  reef11  11864  ghmghmrn  13393  subrgid  13779  znf1o  14207  topopn  14244  fiinbas  14285  topbas  14303  topcld  14345  ntrtop  14364  opnneissb  14391  opnssneib  14392  opnneiid  14400  idcn  14448  cnconst2  14469  lmres  14484  retopbas  14759  cnopncntop  14780  cnopn  14781  abscncf  14821  recncf  14822  imcncf  14823  cjcncf  14824  mulc1cncf  14825  cncfcn1cntop  14830  cncfmpt2fcntop  14835  addccncf  14836  idcncf  14837  sub1cncf  14838  sub2cncf  14839  cdivcncfap  14840  negfcncf  14842  expcncf  14845  cnrehmeocntop  14846  maxcncf  14851  mincncf  14852  ivthreinc  14881  hovercncf  14882  cnlimcim  14907  cnlimc  14908  cnlimci  14909  dvcnp2cntop  14935  dvcn  14936  dvmptfsum  14961  dvef  14963  plyssc  14975  efcn  15004