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