Theorem sssucid 6443

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

Syntax hints:   ∪ cun 3903   ⊆ wss 3905  {csn 4589  suc csuc 6362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922  df-suc 6366

This theorem is referenced by:  trsuc  6450  limsssuc  7842  oaordi  8527  omeulem1  8563  oelim2  8577  nnaordi  8600  naddcllem  8658  phplem2  9185  php  9187  enp1i  9235  fiint  9282  cantnfval2  9634  cantnfle  9636  cantnfp1lem3  9645  cnfcomlem  9664  ttrclss  9685  ranksuc  9833  fseqenlem1  10004  pwsdompw  10182  fin1a2lem12  10390  canthp1lem2  10633  nosupbnd1  27878  nosupbnd2lem1  27879  noinfbnd1  27893  noinfbnd2lem1  27894  bdaypw2n0bndlem  28656  satfvsucsuc  35857  satffunlem2lem2  35898  satffunlem2  35900  nmulprop  36682  limsucncmpi  36956  finxpreclem3  38039  dfsuccl4  39123  press  39148  suceldisj  39467  insucid  44130  minregex  44260  clsk1independent  44772  grur1cld  44956  suctrALT  45534  suctrALT2VD  45544  suctrALT2  45545  suctrALTcf  45630  suctrALTcfVD  45631  suctrALT3  45632