Metamath Proof Explorer


Theorem onunisuci

Description: An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994)

Ref Expression
Hypothesis on.1 AOn
Assertion onunisuci sucA=A

Proof

Step Hyp Ref Expression
1 on.1 AOn
2 1 ontrci TrA
3 1 elexi AV
4 3 unisuc TrAsucA=A
5 2 4 mpbi sucA=A