Metamath Proof Explorer

Theorem onsseleq

Description: Relationship between subset and membership of an ordinal number. (Contributed by NM, 15-Sep-1995)

Ref Expression
Assertion onsseleq ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ A ∈ B ∨ A = B

Proof

Step Hyp Ref Expression
1 eloni ⊢ A ∈ On → Ord ⁡ A
2 eloni ⊢ B ∈ On → Ord ⁡ B
3 ordsseleq ⊢ Ord ⁡ A ∧ Ord ⁡ B → A ⊆ B ↔ A ∈ B ∨ A = B
4 1 2 3 syl2an ⊢ A ∈ On ∧ B ∈ On → A ⊆ B ↔ A ∈ B ∨ A = B