Theorem sssucid 3050

Description: A class is included in its own successor. Part of Proposition 7.23 of [TakeutiZaring] p. 41 (generalized to arbitrary classes).

Assertion

Ref	Expression
sssucid	|- A (_ suc A

Proof of Theorem sssucid

Step	Hyp	Ref	Expression
1		ssun1 2245	. 2 |- A (_ (A u. {A})
2		df-suc 2981	. 2 |- suc A = (A u. {A})
3	1, 2	sseqtr4i 2146	1 |- A (_ suc A

Syntax hints:   u. cun 2097   (_ wss 2099  {csn 2467  suc csuc 2977

This theorem is referenced by:  suceloni 3170  limsssuc 3204  oaordi 4316  oelim2 4358  ac6sfilem3 4590  ac6sfi 4591  phplem4 4658  php 4660  onomeneq 4665  unifi 4701  fiint 4703  fodomfi 4709  r1pwcl 4833  ranksuc 4846  top2usne 11051  finsschain 11425  fbssint 11626  fcluscomplem 11732  suctrALT 12217

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 998  ax-gen 999  ax-8 1000  ax-10 1002  ax-12 1004  ax-17 1007  ax-4 1009  ax-5o 1011  ax-6o 1014  ax-9o 1159  ax-10o 1177  ax-16 1247  ax-11o 1255  ax-ext 1500

This theorem depends on definitions:  df-bi 145  df-or 222  df-an 223  df-ex 1017  df-sb 1209  df-clab 1506  df-cleq 1511  df-clel 1514  df-v 1858  df-un 2102  df-in 2103  df-ss 2105  df-suc 2981

Copyright terms: Public domain