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  6584  rdgss  6659  fpmg  6960  findcard2d  7201  findcard2sd  7202  f1finf1o  7271  fidcenumlemr  7279  snopfsupp  7307  casef  7435  nnnninf  7473  1idprl  7964  1idpru  7965  ltexprlemm  7974  suplocexprlemmu  8092  indconst1  9313  elq  10038  expcl  11015  serclim0  12096  fsum2d  12227  fsumabs  12257  fsumiun  12269  fprod2d  12415  reef11  12491  ghmghmrn  14125  elcntr  14163  cntrnsg  14176  subrgid  14640  znf1o  15095  psrass1filem  15196  topopn  15267  fiinbas  15308  topbas  15326  topcld  15368  ntrtop  15387  opnneissb  15414  opnssneib  15415  opnneiid  15423  idcn  15471  cnconst2  15492  lmres  15507  retopbas  15782  cnopncntop  15803  cnopn  15804  abscncf  15844  recncf  15845  imcncf  15846  cjcncf  15847  mulc1cncf  15848  cncfcn1cntop  15853  cncfmpt2fcntop  15858  addccncf  15859  idcncf  15860  sub1cncf  15861  sub2cncf  15862  cdivcncfap  15863  negfcncf  15865  expcncf  15868  cnrehmeocntop  15869  maxcncf  15874  mincncf  15875  ivthreinc  15904  hovercncf  15905  cnlimcim  15930  cnlimc  15931  cnlimci  15932  dvcnp2cntop  15958  dvcn  15959  dvmptfsum  15984  dvef  15986  plyssc  15998  efcn  16027  uhgrsubgrself  16745  uhgrspansubgr  16756  domomsubct  17269