Theorem ssid 3112

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

Syntax hints:   ∈ wcel 1480   ⊆ wss 3066

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 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-11 1484  ax-4 1487  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2119

This theorem depends on definitions:  df-bi 116  df-nf 1437  df-sb 1736  df-clab 2124  df-cleq 2130  df-clel 2133  df-in 3072  df-ss 3079

This theorem is referenced by:  ssidd  3113  eqimssi  3148  eqimss2i  3149  inv1  3394  difid  3426  undifabs  3434  pwidg  3519  elssuni  3759  unimax  3765  intmin  3786  rintm  3900  iunpw  4396  sucprcreg  4459  tfisi  4496  peano5  4507  xpss1  4644  xpss2  4645  residm  4846  resdm  4853  resmpt3  4863  ssrnres  4976  cocnvss  5059  dffn3  5278  fimacnv  5542  foima2  5646  tfrlem1  6198  rdgss  6273  fpmg  6561  findcard2d  6778  findcard2sd  6779  f1finf1o  6828  fidcenumlemr  6836  casef  6966  nnnninf  7016  1idprl  7391  1idpru  7392  ltexprlemm  7401  suplocexprlemmu  7519  elq  9407  expcl  10304  serclim0  11067  fsum2d  11197  fsumabs  11227  fsumiun  11239  reef11  11395  ressid  12009  topopn  12164  fiinbas  12205  topbas  12225  topcld  12267  ntrtop  12286  opnneissb  12313  opnssneib  12314  opnneiid  12322  idcn  12370  cnconst2  12391  lmres  12406  retopbas  12681  cnopncntop  12695  abscncf  12730  recncf  12731  imcncf  12732  cjcncf  12733  mulc1cncf  12734  cncfcn1cntop  12739  cncfmpt2fcntop  12743  addccncf  12744  cdivcncfap  12745  negfcncf  12747  expcncf  12750  cnrehmeocntop  12751  cnlimcim  12798  cnlimc  12799  cnlimci  12800  dvcnp2cntop  12821  dvcn  12822  dvef  12845  efcn  12846