Theorem sssucid 6150

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 4075	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝐴})
2		df-suc 6079	. 2 ⊢ suc 𝐴 = (𝐴 ∪ {𝐴})
3	1, 2	sseqtr4i 3931	1 ⊢ 𝐴 ⊆ suc 𝐴

Syntax hints:   ∪ cun 3863   ⊆ wss 3865  {csn 4478  suc csuc 6075

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-v 3442  df-un 3870  df-in 3872  df-ss 3880  df-suc 6079

This theorem is referenced by:  trsuc  6157  suceloni  7391  limsssuc  7428  oaordi  8029  omeulem1  8065  oelim2  8078  nnaordi  8101  phplem4  8553  php  8555  onomeneq  8561  fiint  8648  cantnfval2  8985  cantnfle  8987  cantnfp1lem3  8996  cnfcomlem  9015  ranksuc  9147  fseqenlem1  9303  pwsdompw  9479  fin1a2lem12  9686  canthp1lem2  9928  satfvsucsuc  32222  satffunlem2lem2  32263  satffunlem2  32265  nosupbday  32816  nosupbnd1  32825  nosupbnd2lem1  32826  limsucncmpi  33404  finxpreclem3  34226  clsk1independent  39902  grur1cld  40086  suctrALT  40720  suctrALT2VD  40730  suctrALT2  40731  suctrALTcf  40816  suctrALTcfVD  40817  suctrALT3  40818