Theorem sssucid 6328

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 4102	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝐴})
2		df-suc 6257	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
3	1, 2	sseqtrri 3954	1 ⊢ 𝐴 ⊆ suc 𝐴

Syntax hints:   ∪ cun 3881   ⊆ wss 3883  {csn 4558  suc csuc 6253

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900  df-suc 6257

This theorem is referenced by:  trsuc  6335  suceloni  7635  limsssuc  7672  oaordi  8339  omeulem1  8375  oelim2  8388  nnaordi  8411  phplem4  8895  php  8897  onomeneq  8943  fiint  9021  cantnfval2  9357  cantnfle  9359  cantnfp1lem3  9368  cnfcomlem  9387  ranksuc  9554  fseqenlem1  9711  pwsdompw  9891  fin1a2lem12  10098  canthp1lem2  10340  satfvsucsuc  33227  satffunlem2lem2  33268  satffunlem2  33270  ttrclss  33706  naddcllem  33758  nosupbnd1  33844  nosupbnd2lem1  33845  noinfbnd1  33859  noinfbnd2lem1  33860  limsucncmpi  34561  finxpreclem3  35491  clsk1independent  41545  grur1cld  41739  suctrALT  42335  suctrALT2VD  42345  suctrALT2  42346  suctrALTcf  42431  suctrALTcfVD  42432  suctrALT3  42433