Theorem ssid 3175

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

Syntax hints:   ∈ wcel 2148   ⊆ wss 3129

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 3135  df-ss 3142

This theorem is referenced by:  ssidd  3176  eqimssi  3211  eqimss2i  3212  inv1  3459  difid  3491  undifabs  3499  pwidg  3589  elssuni  3837  unimax  3843  intmin  3864  rintm  3979  iunpw  4480  sucprcreg  4548  tfisi  4586  peano5  4597  xpss1  4736  xpss2  4737  residm  4939  resdm  4946  resmpt3  4956  ssrnres  5071  cocnvss  5154  dffn3  5376  fimacnv  5645  foima2  5752  tfrlem1  6308  rdgss  6383  fpmg  6673  findcard2d  6890  findcard2sd  6891  f1finf1o  6945  fidcenumlemr  6953  casef  7086  nnnninf  7123  1idprl  7588  1idpru  7589  ltexprlemm  7598  suplocexprlemmu  7716  elq  9621  expcl  10537  serclim0  11312  fsum2d  11442  fsumabs  11472  fsumiun  11484  fprod2d  11630  reef11  11706  subrgid  13342  topopn  13478  fiinbas  13519  topbas  13537  topcld  13579  ntrtop  13598  opnneissb  13625  opnssneib  13626  opnneiid  13634  idcn  13682  cnconst2  13703  lmres  13718  retopbas  13993  cnopncntop  14007  abscncf  14042  recncf  14043  imcncf  14044  cjcncf  14045  mulc1cncf  14046  cncfcn1cntop  14051  cncfmpt2fcntop  14055  addccncf  14056  cdivcncfap  14057  negfcncf  14059  expcncf  14062  cnrehmeocntop  14063  cnlimcim  14110  cnlimc  14111  cnlimci  14112  dvcnp2cntop  14133  dvcn  14134  dvef  14158  efcn  14159