Theorem ssid 3244

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

Syntax hints:   ∈ wcel 2200   ⊆ wss 3197

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 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-11 1552  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211

This theorem depends on definitions:  df-bi 117  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-in 3203  df-ss 3210

This theorem is referenced by:  ssidd  3245  eqimssi  3280  eqimss2i  3281  inv1  3528  difid  3560  undifabs  3568  pwidg  3663  elssuni  3915  unimax  3921  intmin  3942  rintm  4057  iunpw  4568  sucprcreg  4638  tfisi  4676  peano5  4687  xpss1  4826  xpss2  4827  residm  5033  resdm  5040  resmpt3  5050  ssrnres  5167  cocnvss  5250  dffn3  5480  fimacnv  5757  foima2  5868  tfrlem1  6444  rdgss  6519  fpmg  6811  findcard2d  7041  findcard2sd  7042  f1finf1o  7102  fidcenumlemr  7110  casef  7243  nnnninf  7281  1idprl  7765  1idpru  7766  ltexprlemm  7775  suplocexprlemmu  7893  elq  9805  expcl  10766  serclim0  11802  fsum2d  11932  fsumabs  11962  fsumiun  11974  fprod2d  12120  reef11  12196  ghmghmrn  13786  subrgid  14172  znf1o  14600  topopn  14667  fiinbas  14708  topbas  14726  topcld  14768  ntrtop  14787  opnneissb  14814  opnssneib  14815  opnneiid  14823  idcn  14871  cnconst2  14892  lmres  14907  retopbas  15182  cnopncntop  15203  cnopn  15204  abscncf  15244  recncf  15245  imcncf  15246  cjcncf  15247  mulc1cncf  15248  cncfcn1cntop  15253  cncfmpt2fcntop  15258  addccncf  15259  idcncf  15260  sub1cncf  15261  sub2cncf  15262  cdivcncfap  15263  negfcncf  15265  expcncf  15268  cnrehmeocntop  15269  maxcncf  15274  mincncf  15275  ivthreinc  15304  hovercncf  15305  cnlimcim  15330  cnlimc  15331  cnlimci  15332  dvcnp2cntop  15358  dvcn  15359  dvmptfsum  15384  dvef  15386  plyssc  15398  efcn  15427  domomsubct  16298