Theorem ssid 3291

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	⊢ A ⊆ A

Proof of Theorem ssid

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (x ∈ A → x ∈ A)
2	1	ssriv 3278	1 ⊢ A ⊆ A

Syntax hints:   ∈ wcel 1710   ⊆ wss 3258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-v 2862  df-nin 3212  df-compl 3213  df-in 3214  df-ss 3260

This theorem is referenced by:  eqimssi  3326  eqimss2i  3327  nsspssun  3489  inv1  3578  disjpss  3602  difid  3619  pwidg  3735  elssuni  3920  unimax  3926  intmin  3947  rintn0  4057  ssbri  4682  xpss1  4857  xpss2  4858  residm  4995  resdm  4999  dffn3  5230  fimacnv  5412  clos1nrel  5887  ssetpov  5945  lecidg  6197  sbthlem1  6204