Theorem sssucid 6471

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

This proof depends on syntax axioms:   ⊆ wss 3900   ∪ cun 4152  {csn 4588  suc csuc 6390

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154  df-suc 6394

This theorem is used by:  trsuc  6478  limsssuc  7895  oaordi  8592  omeulem1  8628  oelim2  8642  nnaordi  8665  naddcllem  8723  phplem2  9258  php  9260  enp1i  9308  fiint  9356  cantnfval2  9707  cantnfle  9709  cantnfp1lem3  9718  cnfcomlem  9737  ttrclss  9758  ranksuc  9919  fseqenlem1  10142  pwsdompw  10320  fin1a2lem12  10528  canthp1lem2  10777  nosupbnd1  28128  nosupbnd2lem1  28129  noinfbnd1  28143  noinfbnd2lem1  28144  bdaypw2n0bndlem  28906  satfvsucsuc  36338  satffunlem2lem2  36379  satffunlem2  36381  nmulprop  37154  limsucncmpi  37448  finxpreclem3  38584  dfsuccl4  39672  press  39697  suceldisj  40016  insucid  44666  minregex  44796  clsk1independent  45307  grur1cld  45491  suctrALT  46068  suctrALT2VD  46078  suctrALT2  46079  suctrALTcf  46164  suctrALTcfVD  46165  suctrALT3  46166