Metamath Proof Explorer

Theorem ssonunii

Description: The union of a set of ordinal numbers is an ordinal number. Corollary 7N(d) of Enderton p. 193. (Contributed by NM, 20-Sep-2003)

Ref Expression
Hypothesis ssonuni.1 
|- A e. _V
Assertion ssonunii 
|- ( A C_ On -> U. A e. On )

Proof

Step Hyp Ref Expression
1 ssonuni.1 
 |-  A e. _V
2 ssonuni 
 |-  ( A e. _V -> ( A C_ On -> U. A e. On ) )
3 1 2 ax-mp 
 |-  ( A C_ On -> U. A e. On )