Theorem ssid 3122

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

Syntax hints:   ∈ wcel 1481   ⊆ wss 3076

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-11 1485  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-in 3082  df-ss 3089

This theorem is referenced by:  ssidd  3123  eqimssi  3158  eqimss2i  3159  inv1  3404  difid  3436  undifabs  3444  pwidg  3529  elssuni  3772  unimax  3778  intmin  3799  rintm  3913  iunpw  4409  sucprcreg  4472  tfisi  4509  peano5  4520  xpss1  4657  xpss2  4658  residm  4859  resdm  4866  resmpt3  4876  ssrnres  4989  cocnvss  5072  dffn3  5291  fimacnv  5557  foima2  5661  tfrlem1  6213  rdgss  6288  fpmg  6576  findcard2d  6793  findcard2sd  6794  f1finf1o  6843  fidcenumlemr  6851  casef  6981  nnnninf  7031  1idprl  7422  1idpru  7423  ltexprlemm  7432  suplocexprlemmu  7550  elq  9441  expcl  10342  serclim0  11106  fsum2d  11236  fsumabs  11266  fsumiun  11278  reef11  11442  ressid  12059  topopn  12214  fiinbas  12255  topbas  12275  topcld  12317  ntrtop  12336  opnneissb  12363  opnssneib  12364  opnneiid  12372  idcn  12420  cnconst2  12441  lmres  12456  retopbas  12731  cnopncntop  12745  abscncf  12780  recncf  12781  imcncf  12782  cjcncf  12783  mulc1cncf  12784  cncfcn1cntop  12789  cncfmpt2fcntop  12793  addccncf  12794  cdivcncfap  12795  negfcncf  12797  expcncf  12800  cnrehmeocntop  12801  cnlimcim  12848  cnlimc  12849  cnlimci  12850  dvcnp2cntop  12871  dvcn  12872  dvef  12896  efcn  12897