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