Theorem ssid 3247

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

Syntax hints:   ∈ wcel 2202   ⊆ wss 3200

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 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-11 1554  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3206  df-ss 3213

This theorem is referenced by:  ssidd  3248  eqimssi  3283  eqimss2i  3284  inv1  3531  difid  3563  undifabs  3571  pwidg  3666  elssuni  3921  unimax  3927  intmin  3948  rintm  4063  iunpw  4577  sucprcreg  4647  tfisi  4685  peano5  4696  xpss1  4836  xpss2  4837  residm  5045  resdm  5052  resmpt3  5062  ssrnres  5179  cocnvss  5262  dffn3  5493  fimacnv  5776  foima2  5892  tfrlem1  6474  rdgss  6549  fpmg  6843  findcard2d  7080  findcard2sd  7081  f1finf1o  7146  fidcenumlemr  7154  casef  7287  nnnninf  7325  1idprl  7810  1idpru  7811  ltexprlemm  7820  suplocexprlemmu  7938  elq  9856  expcl  10819  serclim0  11866  fsum2d  11997  fsumabs  12027  fsumiun  12039  fprod2d  12185  reef11  12261  ghmghmrn  13851  subrgid  14239  znf1o  14667  topopn  14734  fiinbas  14775  topbas  14793  topcld  14835  ntrtop  14854  opnneissb  14881  opnssneib  14882  opnneiid  14890  idcn  14938  cnconst2  14959  lmres  14974  retopbas  15249  cnopncntop  15270  cnopn  15271  abscncf  15311  recncf  15312  imcncf  15313  cjcncf  15314  mulc1cncf  15315  cncfcn1cntop  15320  cncfmpt2fcntop  15325  addccncf  15326  idcncf  15327  sub1cncf  15328  sub2cncf  15329  cdivcncfap  15330  negfcncf  15332  expcncf  15335  cnrehmeocntop  15336  maxcncf  15341  mincncf  15342  ivthreinc  15371  hovercncf  15372  cnlimcim  15397  cnlimc  15398  cnlimci  15399  dvcnp2cntop  15425  dvcn  15426  dvmptfsum  15451  dvef  15453  plyssc  15465  efcn  15494  uhgrsubgrself  16119  uhgrspansubgr  16130  domomsubct  16605