Theorem ssid 1519

Description: Any class is a subclass of itself. Exercise 10 of [TakeutiZaring] p. 18.

Assertion

Ref	Expression
ssid	⊢ A ⊆ A

Proof of Theorem ssid

Step	Hyp	Ref	Expression
1		cleqid 1102	. . 3 ⊢ A = A
2		eqss 1516	. . 3 ⊢ (A = A ↔ (A ⊆ A ∧ A ⊆ A))
3	1, 2	mpbi 164	. 2 ⊢ (A ⊆ A ∧ A ⊆ A)
4	3	pm3.26i 257	1 ⊢ A ⊆ A

Syntax hints:   ∧ wa 196   = wceq 1091   ⊆ wss 1487

This theorem is referenced by:  eqimss 1548  nssinpss 1665  nsspssun 1666  inv 1723  disjpss 1738  difid 1755  pwid 1805  elssuni 1940  unisseq 1946  intmin 1982  iunpw 2040  ordunidif 2260  onsucuni 2335  ssres2 2590  resabs2 2593  residm 2594  funi 2692  fnfrn 2758  fssxp 2761  tfrlem1 2949  tz7.48-2 2995  abianfp 3000  oaordi 3148  nnmordi 3188  xpdom3 3347  sucprcreg 3451  scott0 3542  zornlem4 3606  htalem 3618  cflem 3700  cflecard 3707  axresscn 4062  expclt 4696  fac0 4871  xpnnen 4927  alephexp2 4956  helch 5151  occlt 5189  omls 5251  shintclt 5295  chintclt 5297  shlesb1 5360  chm1 5378  chlejb1 5397  chm0 5411  chabs1t 5432  chabs2t 5433  cmid 5516  pjidmco 5642

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-16 922  ax-17 925  ax-ext 1074

This theorem depends on definitions:  df-bi 128  df-an 198  df-ex 679  df-sb 853  df-clab 1093  df-cleq 1097  df-clel 1099  df-in 1491  df-ss 1492

metamath.org