Theorem sssucid 6445

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

Syntax hints:   ∪ cun 3947   ⊆ wss 3949  {csn 4629  suc csuc 6367

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 3954  df-in 3956  df-ss 3966  df-suc 6371

This theorem is referenced by:  trsuc  6452  sucexeloniOLD  7798  suceloniOLD  7800  limsssuc  7839  oaordi  8546  omeulem1  8582  oelim2  8595  nnaordi  8618  naddcllem  8675  phplem2  9208  php  9210  phplem4OLD  9220  phpOLD  9222  onomeneqOLD  9229  enp1i  9279  fiint  9324  cantnfval2  9664  cantnfle  9666  cantnfp1lem3  9675  cnfcomlem  9694  ttrclss  9715  ranksuc  9860  fseqenlem1  10019  pwsdompw  10199  fin1a2lem12  10406  canthp1lem2  10648  nosupbnd1  27217  nosupbnd2lem1  27218  noinfbnd1  27232  noinfbnd2lem1  27233  satfvsucsuc  34356  satffunlem2lem2  34397  satffunlem2  34399  limsucncmpi  35330  finxpreclem3  36274  insucid  42154  minregex  42285  clsk1independent  42797  grur1cld  42991  suctrALT  43587  suctrALT2VD  43597  suctrALT2  43598  suctrALTcf  43683  suctrALTcfVD  43684  suctrALT3  43685