Metamath Proof Explorer


Theorem onssi

Description: An ordinal number is a subset of On . (Contributed by NM, 11-Aug-1994)

Ref Expression
Hypothesis onssi.1
|- A e. On
Assertion onssi
|- A C_ On

Proof

Step Hyp Ref Expression
1 onssi.1
 |-  A e. On
2 onss
 |-  ( A e. On -> A C_ On )
3 1 2 ax-mp
 |-  A C_ On