Theorem sssucid 6389

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

Syntax hints:   ∪ cun 3901   ⊆ wss 3903  {csn 4577  suc csuc 6309

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3438  df-un 3908  df-ss 3920  df-suc 6313

This theorem is referenced by:  trsuc  6396  limsssuc  7783  oaordi  8464  omeulem1  8500  oelim2  8513  nnaordi  8536  naddcllem  8594  phplem2  9119  php  9121  enp1i  9168  fiint  9216  fiintOLD  9217  cantnfval2  9565  cantnfle  9567  cantnfp1lem3  9576  cnfcomlem  9595  ttrclss  9616  ranksuc  9761  fseqenlem1  9918  pwsdompw  10097  fin1a2lem12  10305  canthp1lem2  10547  nosupbnd1  27624  nosupbnd2lem1  27625  noinfbnd1  27639  noinfbnd2lem1  27640  satfvsucsuc  35338  satffunlem2lem2  35379  satffunlem2  35381  limsucncmpi  36419  finxpreclem3  37367  insucid  43376  minregex  43507  clsk1independent  44019  grur1cld  44205  suctrALT  44799  suctrALT2VD  44809  suctrALT2  44810  suctrALTcf  44895  suctrALTcfVD  44896  suctrALT3  44897