Theorem ssid 3215

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

Syntax hints:   ∈ wcel 2177   ⊆ wss 3168

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 1471  ax-7 1472  ax-gen 1473  ax-ie1 1517  ax-ie2 1518  ax-8 1528  ax-11 1530  ax-4 1534  ax-17 1550  ax-i9 1554  ax-ial 1558  ax-i5r 1559  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-nf 1485  df-sb 1787  df-clab 2193  df-cleq 2199  df-clel 2202  df-in 3174  df-ss 3181

This theorem is referenced by:  ssidd  3216  eqimssi  3251  eqimss2i  3252  inv1  3499  difid  3531  undifabs  3539  pwidg  3632  elssuni  3881  unimax  3887  intmin  3908  rintm  4023  iunpw  4532  sucprcreg  4602  tfisi  4640  peano5  4651  xpss1  4790  xpss2  4791  residm  4997  resdm  5004  resmpt3  5014  ssrnres  5131  cocnvss  5214  dffn3  5443  fimacnv  5719  foima2  5830  tfrlem1  6404  rdgss  6479  fpmg  6771  findcard2d  7000  findcard2sd  7001  f1finf1o  7061  fidcenumlemr  7069  casef  7202  nnnninf  7240  1idprl  7716  1idpru  7717  ltexprlemm  7726  suplocexprlemmu  7844  elq  9756  expcl  10715  serclim0  11666  fsum2d  11796  fsumabs  11826  fsumiun  11838  fprod2d  11984  reef11  12060  ghmghmrn  13649  subrgid  14035  znf1o  14463  topopn  14530  fiinbas  14571  topbas  14589  topcld  14631  ntrtop  14650  opnneissb  14677  opnssneib  14678  opnneiid  14686  idcn  14734  cnconst2  14755  lmres  14770  retopbas  15045  cnopncntop  15066  cnopn  15067  abscncf  15107  recncf  15108  imcncf  15109  cjcncf  15110  mulc1cncf  15111  cncfcn1cntop  15116  cncfmpt2fcntop  15121  addccncf  15122  idcncf  15123  sub1cncf  15124  sub2cncf  15125  cdivcncfap  15126  negfcncf  15128  expcncf  15131  cnrehmeocntop  15132  maxcncf  15137  mincncf  15138  ivthreinc  15167  hovercncf  15168  cnlimcim  15193  cnlimc  15194  cnlimci  15195  dvcnp2cntop  15221  dvcn  15222  dvmptfsum  15247  dvef  15249  plyssc  15261  efcn  15290  domomsubct  16053