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 𝐴 ∈ On
Assertion onssi 𝐴 ⊆ On

Proof

Step Hyp Ref Expression
1 onssi.1 𝐴 ∈ On
2 onss ( 𝐴 ∈ On → 𝐴 ⊆ On )
3 1 2 ax-mp 𝐴 ⊆ On