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 e. On -> U. suc A = A )

Proof

Step Hyp Ref Expression
1 ontr
 |-  ( A e. On -> Tr A )
2 unisucg
 |-  ( A e. On -> ( Tr A <-> U. suc A = A ) )
3 1 2 mpbid
 |-  ( A e. On -> U. suc A = A )