Metamath Proof Explorer


Theorem onunisuc

Description: An ordinal number is equal to the union of its successor. (Contributed by NM, 12-Jun-1994) Generalize from onunisuci . (Revised by BJ, 28-Dec-2024)

Ref Expression
Assertion onunisuc A On suc A = A

Proof

Step Hyp Ref Expression
1 ontr A On Tr A
2 unisucg A On Tr A suc A = A
3 1 2 mpbid A On suc A = A