Theorem ssid 3187

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

Syntax hints:   ∈ wcel 2158   ⊆ wss 3141

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 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-11 1516  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2169

This theorem depends on definitions:  df-bi 117  df-nf 1471  df-sb 1773  df-clab 2174  df-cleq 2180  df-clel 2183  df-in 3147  df-ss 3154

This theorem is referenced by:  ssidd  3188  eqimssi  3223  eqimss2i  3224  inv1  3471  difid  3503  undifabs  3511  pwidg  3601  elssuni  3849  unimax  3855  intmin  3876  rintm  3991  iunpw  4492  sucprcreg  4560  tfisi  4598  peano5  4609  xpss1  4748  xpss2  4749  residm  4951  resdm  4958  resmpt3  4968  ssrnres  5083  cocnvss  5166  dffn3  5388  fimacnv  5658  foima2  5765  tfrlem1  6323  rdgss  6398  fpmg  6688  findcard2d  6905  findcard2sd  6906  f1finf1o  6960  fidcenumlemr  6968  casef  7101  nnnninf  7138  1idprl  7603  1idpru  7604  ltexprlemm  7613  suplocexprlemmu  7731  elq  9636  expcl  10552  serclim0  11327  fsum2d  11457  fsumabs  11487  fsumiun  11499  fprod2d  11645  reef11  11721  ghmghmrn  13157  subrgid  13500  topopn  13861  fiinbas  13902  topbas  13920  topcld  13962  ntrtop  13981  opnneissb  14008  opnssneib  14009  opnneiid  14017  idcn  14065  cnconst2  14086  lmres  14101  retopbas  14376  cnopncntop  14390  abscncf  14425  recncf  14426  imcncf  14427  cjcncf  14428  mulc1cncf  14429  cncfcn1cntop  14434  cncfmpt2fcntop  14438  addccncf  14439  cdivcncfap  14440  negfcncf  14442  expcncf  14445  cnrehmeocntop  14446  cnlimcim  14493  cnlimc  14494  cnlimci  14495  dvcnp2cntop  14516  dvcn  14517  dvef  14541  efcn  14542