Theorem sssucid 6442

Description: A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes). (Contributed by NM, 31-May-1994.)

Assertion

Ref	Expression
sssucid	⊢ 𝐴 ⊆ suc 𝐴

Proof of Theorem sssucid

Step	Hyp	Ref	Expression
1		ssun1 4172	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝐴})
2		df-suc 6368	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
3	1, 2	sseqtrri 4019	1 ⊢ 𝐴 ⊆ suc 𝐴

Syntax hints:   ∪ cun 3946   ⊆ wss 3948  {csn 4628  suc csuc 6364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3953  df-in 3955  df-ss 3965  df-suc 6368

This theorem is referenced by:  trsuc  6449  sucexeloniOLD  7795  suceloniOLD  7797  limsssuc  7836  oaordi  8543  omeulem1  8579  oelim2  8592  nnaordi  8615  naddcllem  8672  phplem2  9205  php  9207  phplem4OLD  9217  phpOLD  9219  onomeneqOLD  9226  enp1i  9276  fiint  9321  cantnfval2  9661  cantnfle  9663  cantnfp1lem3  9672  cnfcomlem  9691  ttrclss  9712  ranksuc  9857  fseqenlem1  10016  pwsdompw  10196  fin1a2lem12  10403  canthp1lem2  10645  nosupbnd1  27207  nosupbnd2lem1  27208  noinfbnd1  27222  noinfbnd2lem1  27223  satfvsucsuc  34345  satffunlem2lem2  34386  satffunlem2  34388  limsucncmpi  35319  finxpreclem3  36263  insucid  42140  minregex  42271  clsk1independent  42783  grur1cld  42977  suctrALT  43573  suctrALT2VD  43583  suctrALT2  43584  suctrALTcf  43669  suctrALTcfVD  43670  suctrALT3  43671