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

Proof

Step Hyp Ref Expression
1 on.1
 |-  A e. On
2 1 ontrci
 |-  Tr A
3 1 elexi
 |-  A e. _V
4 3 unisuc
 |-  ( Tr A <-> U. suc A = A )
5 2 4 mpbi
 |-  U. suc A = A