Theorem ssid 3176

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

Syntax hints:   ∈ wcel 2148   ⊆ wss 3130

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-11 1506  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159

This theorem depends on definitions:  df-bi 117  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-in 3136  df-ss 3143

This theorem is referenced by:  ssidd  3177  eqimssi  3212  eqimss2i  3213  inv1  3460  difid  3492  undifabs  3500  pwidg  3590  elssuni  3838  unimax  3844  intmin  3865  rintm  3980  iunpw  4481  sucprcreg  4549  tfisi  4587  peano5  4598  xpss1  4737  xpss2  4738  residm  4940  resdm  4947  resmpt3  4957  ssrnres  5072  cocnvss  5155  dffn3  5377  fimacnv  5646  foima2  5753  tfrlem1  6309  rdgss  6384  fpmg  6674  findcard2d  6891  findcard2sd  6892  f1finf1o  6946  fidcenumlemr  6954  casef  7087  nnnninf  7124  1idprl  7589  1idpru  7590  ltexprlemm  7599  suplocexprlemmu  7717  elq  9622  expcl  10538  serclim0  11313  fsum2d  11443  fsumabs  11473  fsumiun  11485  fprod2d  11631  reef11  11707  subrgid  13344  topopn  13511  fiinbas  13552  topbas  13570  topcld  13612  ntrtop  13631  opnneissb  13658  opnssneib  13659  opnneiid  13667  idcn  13715  cnconst2  13736  lmres  13751  retopbas  14026  cnopncntop  14040  abscncf  14075  recncf  14076  imcncf  14077  cjcncf  14078  mulc1cncf  14079  cncfcn1cntop  14084  cncfmpt2fcntop  14088  addccncf  14089  cdivcncfap  14090  negfcncf  14092  expcncf  14095  cnrehmeocntop  14096  cnlimcim  14143  cnlimc  14144  cnlimci  14145  dvcnp2cntop  14166  dvcn  14167  dvef  14191  efcn  14192