Theorem ssid 3257

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

Syntax hints:   ∈ wcel 2203   ⊆ wss 3210

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 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-11 1555  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-in 3216  df-ss 3223

This theorem is referenced by:  ssidd  3258  eqimssi  3293  eqimss2i  3294  inv1  3544  difid  3576  undifabs  3585  pwidg  3685  elssuni  3941  unimax  3947  intmin  3968  rintm  4083  iunpw  4600  sucprcreg  4670  tfisi  4708  peano5  4719  xpss1  4859  xpss2  4860  residm  5069  resdm  5076  resmpt3  5086  ssrnres  5204  cocnvss  5287  dffn3  5518  fimacnv  5805  foima2  5923  tfrlem1  6538  rdgss  6613  fpmg  6907  findcard2d  7147  findcard2sd  7148  f1finf1o  7216  fidcenumlemr  7224  casef  7378  nnnninf  7416  1idprl  7904  1idpru  7905  ltexprlemm  7914  suplocexprlemmu  8032  elq  9953  expcl  10918  serclim0  11986  fsum2d  12117  fsumabs  12147  fsumiun  12159  fprod2d  12305  reef11  12381  ghmghmrn  13972  subrgid  14360  znf1o  14791  topopn  14865  fiinbas  14906  topbas  14924  topcld  14966  ntrtop  14985  opnneissb  15012  opnssneib  15013  opnneiid  15021  idcn  15069  cnconst2  15090  lmres  15105  retopbas  15380  cnopncntop  15401  cnopn  15402  abscncf  15442  recncf  15443  imcncf  15444  cjcncf  15445  mulc1cncf  15446  cncfcn1cntop  15451  cncfmpt2fcntop  15456  addccncf  15457  idcncf  15458  sub1cncf  15459  sub2cncf  15460  cdivcncfap  15461  negfcncf  15463  expcncf  15466  cnrehmeocntop  15467  maxcncf  15472  mincncf  15473  ivthreinc  15502  hovercncf  15503  cnlimcim  15528  cnlimc  15529  cnlimci  15530  dvcnp2cntop  15556  dvcn  15557  dvmptfsum  15582  dvef  15584  plyssc  15596  efcn  15625  uhgrsubgrself  16253  uhgrspansubgr  16264  domomsubct  16767