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 )