Theorem ssid 3248

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

Syntax hints:   ∈ wcel 2202   ⊆ wss 3201

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 2213

This theorem depends on definitions:  df-bi 117  df-nf 1510  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-in 3207  df-ss 3214

This theorem is referenced by:  ssidd  3249  eqimssi  3284  eqimss2i  3285  inv1  3533  difid  3565  undifabs  3573  pwidg  3670  elssuni  3926  unimax  3932  intmin  3953  rintm  4068  iunpw  4583  sucprcreg  4653  tfisi  4691  peano5  4702  xpss1  4842  xpss2  4843  residm  5051  resdm  5058  resmpt3  5068  ssrnres  5186  cocnvss  5269  dffn3  5500  fimacnv  5784  foima2  5902  tfrlem1  6517  rdgss  6592  fpmg  6886  findcard2d  7123  findcard2sd  7124  f1finf1o  7189  fidcenumlemr  7197  casef  7330  nnnninf  7368  1idprl  7853  1idpru  7854  ltexprlemm  7863  suplocexprlemmu  7981  elq  9899  expcl  10863  serclim0  11926  fsum2d  12057  fsumabs  12087  fsumiun  12099  fprod2d  12245  reef11  12321  ghmghmrn  13911  subrgid  14299  znf1o  14727  topopn  14799  fiinbas  14840  topbas  14858  topcld  14900  ntrtop  14919  opnneissb  14946  opnssneib  14947  opnneiid  14955  idcn  15003  cnconst2  15024  lmres  15039  retopbas  15314  cnopncntop  15335  cnopn  15336  abscncf  15376  recncf  15377  imcncf  15378  cjcncf  15379  mulc1cncf  15380  cncfcn1cntop  15385  cncfmpt2fcntop  15390  addccncf  15391  idcncf  15392  sub1cncf  15393  sub2cncf  15394  cdivcncfap  15395  negfcncf  15397  expcncf  15400  cnrehmeocntop  15401  maxcncf  15406  mincncf  15407  ivthreinc  15436  hovercncf  15437  cnlimcim  15462  cnlimc  15463  cnlimci  15464  dvcnp2cntop  15490  dvcn  15491  dvmptfsum  15516  dvef  15518  plyssc  15530  efcn  15559  uhgrsubgrself  16187  uhgrspansubgr  16198  domomsubct  16703