Theorem ssid 3268

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

Syntax hints:   ∈ wcel 2209   ⊆ wss 3220

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 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-11 1559  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220

This theorem depends on definitions:  df-bi 117  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-in 3226  df-ss 3233

This theorem is referenced by:  ssidd  3269  eqimssi  3304  eqimss2i  3305  inv1  3559  difid  3594  disjdif  3599  undifabs  3604  pwidg  3705  elssuni  3961  unimax  3967  intmin  3988  rintm  4103  iunpw  4624  sucprcreg  4694  tfisi  4732  peano5  4743  xpss1  4883  xpss2  4884  residm  5093  resdm  5100  resmpt3  5110  ssrnres  5228  cocnvss  5311  dffn3  5542  fimacnv  5831  foima2  5951  fdmrn  6028  tfrlem1  6573  rdgss  6648  fpmg  6949  findcard2d  7189  findcard2sd  7190  f1finf1o  7258  fidcenumlemr  7266  casef  7422  nnnninf  7460  1idprl  7951  1idpru  7952  ltexprlemm  7961  suplocexprlemmu  8079  elq  10005  expcl  10977  serclim0  12054  fsum2d  12185  fsumabs  12215  fsumiun  12227  fprod2d  12373  reef11  12449  ghmghmrn  14049  subrgid  14514  znf1o  14969  topopn  15092  fiinbas  15133  topbas  15151  topcld  15193  ntrtop  15212  opnneissb  15239  opnssneib  15240  opnneiid  15248  idcn  15296  cnconst2  15317  lmres  15332  retopbas  15607  cnopncntop  15628  cnopn  15629  abscncf  15669  recncf  15670  imcncf  15671  cjcncf  15672  mulc1cncf  15673  cncfcn1cntop  15678  cncfmpt2fcntop  15683  addccncf  15684  idcncf  15685  sub1cncf  15686  sub2cncf  15687  cdivcncfap  15688  negfcncf  15690  expcncf  15693  cnrehmeocntop  15694  maxcncf  15699  mincncf  15700  ivthreinc  15729  hovercncf  15730  cnlimcim  15755  cnlimc  15756  cnlimci  15757  dvcnp2cntop  15783  dvcn  15784  dvmptfsum  15809  dvef  15811  plyssc  15823  efcn  15852  uhgrsubgrself  16490  uhgrspansubgr  16501  domomsubct  17014