Theorem onsuci 7854

Description: The successor of an ordinal number is an ordinal number. Inference associated with onsuc 7828 and onsucb 7832. Corollary 7N(c) of [Enderton] p. 193. (Contributed by NM, 12-Jun-1994.)

Hypothesis

Ref	Expression
onssi.1	⊢ 𝐴 ∈ On

Assertion

Ref	Expression
onsuci	⊢ suc 𝐴 ∈ On

Proof of Theorem onsuci

Step	Hyp	Ref	Expression
1		onssi.1	. 2 ⊢ 𝐴 ∈ On
2		onsuc 7828	. 2 ⊢ (𝐴 ∈ On → suc 𝐴 ∈ On)
3	1, 2	ax-mp 5	1 ⊢ suc 𝐴 ∈ On

This proof depends on syntax axioms:   ∈ wcel 2144  Oncon0 6365  suc csuc 6367

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5391  ax-un 7755

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-op 4835  df-uni 4867  df-br 5103  df-opab 5167  df-tr 5212  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-ord 6368  df-on 6369  df-suc 6371

This theorem is used by:  3on  8500  4on  8501  tz9.12lem2  9802  tz9.12  9804  rankpwi  9839  bndrank  9861  rankval4b  9887  rankval4  9891  rankmapu  9902  rankxplim3  9905  cfcof  10359  ttukeylem6  10599  bdayiun  28310  n0bday  28747  bdaypw2n0bndlem  28858  bdaypw2bnd  28860  bdayfinbndlem1  28862  z12bdaylem2  28866  scottssr1  35812  5on  35831  6on  35832  7on  35833  8on  35834  9on  35835  onprcf1acwevdlem2  35969  onsucconni  37321  onsucsuccmpi  37327