Theorem ssid 3268

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

This proof depends on syntax axioms:   ∈ wcel 2209   ⊆ wss 3220

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is used by:  ssidd  3269  eqimssi  3304  eqimss2i  3305  inv1  3559  difid  3594  disjdif  3599  undifabs  3604  pwidg  3706  elssuni  3963  unimax  3969  intmin  3990  rintm  4105  iunpw  4628  sucprcreg  4698  tfisi  4736  peano5  4747  xpss1  4887  xpss2  4888  residm  5097  resdm  5104  resmpt3  5115  ssrnres  5233  cocnvss  5316  dffn3  5547  fimacnv  5840  foima2  5960  fdmrn  6037  tfrlem1  6583  rdgss  6658  fpmg  6959  findcard2d  7200  findcard2sd  7201  f1finf1o  7270  fidcenumlemr  7278  casef  7435  nnnninf  7473  1idprl  7964  1idpru  7965  ltexprlemm  7974  suplocexprlemmu  8092  indconst1  9313  elq  10039  expcl  11016  serclim0  12097  fsum2d  12228  fsumabs  12258  fsumiun  12270  fprod2d  12416  reef11  12492  ghmghmrn  14126  elcntr  14164  cntrnsg  14177  subrgid  14641  znf1o  15096  psrass1filem  15182  topopn  15246  fiinbas  15287  topbas  15305  topcld  15347  ntrtop  15366  opnneissb  15393  opnssneib  15394  opnneiid  15402  idcn  15450  cnconst2  15471  lmres  15486  retopbas  15761  cnopncntop  15782  cnopn  15783  abscncf  15823  recncf  15824  imcncf  15825  cjcncf  15826  mulc1cncf  15827  cncfcn1cntop  15832  cncfmpt2fcntop  15837  addccncf  15838  idcncf  15839  sub1cncf  15840  sub2cncf  15841  cdivcncfap  15842  negfcncf  15844  expcncf  15847  cnrehmeocntop  15848  maxcncf  15853  mincncf  15854  ivthreinc  15883  hovercncf  15884  cnlimcim  15909  cnlimc  15910  cnlimci  15911  dvcnp2cntop  15937  dvcn  15938  dvmptfsum  15963  dvef  15965  plyssc  15977  efcn  16006  uhgrsubgrself  16724  uhgrspansubgr  16735  domomsubct  17248