Theorem ssid 3204

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 3188	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  3205  eqimssi  3240  eqimss2i  3241  inv1  3488  difid  3520  undifabs  3528  pwidg  3620  elssuni  3868  unimax  3874  intmin  3895  rintm  4010  iunpw  4516  sucprcreg  4586  tfisi  4624  peano5  4635  xpss1  4774  xpss2  4775  residm  4979  resdm  4986  resmpt3  4996  ssrnres  5113  cocnvss  5196  dffn3  5421  fimacnv  5694  foima2  5801  tfrlem1  6375  rdgss  6450  fpmg  6742  findcard2d  6961  findcard2sd  6962  f1finf1o  7022  fidcenumlemr  7030  casef  7163  nnnninf  7201  1idprl  7676  1idpru  7677  ltexprlemm  7686  suplocexprlemmu  7804  elq  9715  expcl  10668  serclim0  11489  fsum2d  11619  fsumabs  11649  fsumiun  11661  fprod2d  11807  reef11  11883  ghmghmrn  13471  subrgid  13857  znf1o  14285  topopn  14352  fiinbas  14393  topbas  14411  topcld  14453  ntrtop  14472  opnneissb  14499  opnssneib  14500  opnneiid  14508  idcn  14556  cnconst2  14577  lmres  14592  retopbas  14867  cnopncntop  14888  cnopn  14889  abscncf  14929  recncf  14930  imcncf  14931  cjcncf  14932  mulc1cncf  14933  cncfcn1cntop  14938  cncfmpt2fcntop  14943  addccncf  14944  idcncf  14945  sub1cncf  14946  sub2cncf  14947  cdivcncfap  14948  negfcncf  14950  expcncf  14953  cnrehmeocntop  14954  maxcncf  14959  mincncf  14960  ivthreinc  14989  hovercncf  14990  cnlimcim  15015  cnlimc  15016  cnlimci  15017  dvcnp2cntop  15043  dvcn  15044  dvmptfsum  15069  dvef  15071  plyssc  15083  efcn  15112  domomsubct  15756