This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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