Theorem sssucid 5945

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

Syntax hints:   ∪ cun 3719   ⊆ wss 3721  {csn 4314  suc csuc 5868

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-un 3726  df-in 3728  df-ss 3735  df-suc 5872

This theorem is referenced by:  trsuc  5953  suceloni  7159  limsssuc  7196  oaordi  7779  omeulem1  7815  oelim2  7828  nnaordi  7851  phplem4  8297  php  8299  onomeneq  8305  fiint  8392  cantnfval2  8729  cantnfle  8731  cantnfp1lem3  8740  cnfcomlem  8759  ranksuc  8891  fseqenlem1  9046  pwsdompw  9227  fin1a2lem12  9434  canthp1lem2  9676  nosupbday  32182  nosupbnd1  32191  nosupbnd2lem1  32192  limsucncmpi  32775  finxpreclem3  33560  clsk1independent  38863  suctrALT  39577  suctrALT2VD  39587  suctrALT2  39588  suctrALTcf  39674  suctrALTcfVD  39675  suctrALT3  39676