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  3836  unimax  3842  intmin  3863  rintm  3977  iunpw  4478  sucprcreg  4546  tfisi  4584  peano5  4595  xpss1  4734  xpss2  4735  residm  4936  resdm  4943  resmpt3  4953  ssrnres  5068  cocnvss  5151  dffn3  5373  fimacnv  5642  foima2  5748  tfrlem1  6304  rdgss  6379  fpmg  6669  findcard2d  6886  findcard2sd  6887  f1finf1o  6941  fidcenumlemr  6949  casef  7082  nnnninf  7119  1idprl  7584  1idpru  7585  ltexprlemm  7594  suplocexprlemmu  7712  elq  9616  expcl  10531  serclim0  11304  fsum2d  11434  fsumabs  11464  fsumiun  11476  fprod2d  11622  reef11  11698  topopn  13288  fiinbas  13329  topbas  13349  topcld  13391  ntrtop  13410  opnneissb  13437  opnssneib  13438  opnneiid  13446  idcn  13494  cnconst2  13515  lmres  13530  retopbas  13805  cnopncntop  13819  abscncf  13854  recncf  13855  imcncf  13856  cjcncf  13857  mulc1cncf  13858  cncfcn1cntop  13863  cncfmpt2fcntop  13867  addccncf  13868  cdivcncfap  13869  negfcncf  13871  expcncf  13874  cnrehmeocntop  13875  cnlimcim  13922  cnlimc  13923  cnlimci  13924  dvcnp2cntop  13945  dvcn  13946  dvef  13970  efcn  13971