Theorem ssid 3262

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

Syntax hints:   ∈ wcel 2205   ⊆ wss 3214

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 2216

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-in 3220  df-ss 3227

This theorem is referenced by:  ssidd  3263  eqimssi  3298  eqimss2i  3299  inv1  3549  difid  3581  undifabs  3590  pwidg  3691  elssuni  3947  unimax  3953  intmin  3974  rintm  4089  iunpw  4606  sucprcreg  4676  tfisi  4714  peano5  4725  xpss1  4865  xpss2  4866  residm  5075  resdm  5082  resmpt3  5092  ssrnres  5210  cocnvss  5293  dffn3  5524  fimacnv  5811  foima2  5930  fdmrn  6007  tfrlem1  6552  rdgss  6627  fpmg  6921  findcard2d  7161  findcard2sd  7162  f1finf1o  7230  fidcenumlemr  7238  casef  7392  nnnninf  7430  1idprl  7921  1idpru  7922  ltexprlemm  7931  suplocexprlemmu  8049  elq  9972  expcl  10943  serclim0  12015  fsum2d  12146  fsumabs  12176  fsumiun  12188  fprod2d  12334  reef11  12410  ghmghmrn  14064  subrgid  14454  znf1o  14911  topopn  14985  fiinbas  15026  topbas  15044  topcld  15086  ntrtop  15105  opnneissb  15132  opnssneib  15133  opnneiid  15141  idcn  15189  cnconst2  15210  lmres  15225  retopbas  15500  cnopncntop  15521  cnopn  15522  abscncf  15562  recncf  15563  imcncf  15564  cjcncf  15565  mulc1cncf  15566  cncfcn1cntop  15571  cncfmpt2fcntop  15576  addccncf  15577  idcncf  15578  sub1cncf  15579  sub2cncf  15580  cdivcncfap  15581  negfcncf  15583  expcncf  15586  cnrehmeocntop  15587  maxcncf  15592  mincncf  15593  ivthreinc  15622  hovercncf  15623  cnlimcim  15648  cnlimc  15649  cnlimci  15650  dvcnp2cntop  15676  dvcn  15677  dvmptfsum  15702  dvef  15704  plyssc  15716  efcn  15745  uhgrsubgrself  16373  uhgrspansubgr  16384  domomsubct  16887