Metamath Proof Explorer


Theorem rightno

Description: An element of a right set is a surreal. (Contributed by Scott Fenton, 27-Feb-2026)

Ref Expression
Assertion rightno ⊢ A ∈ R ⁡ B → A ∈ No

Proof

Step Hyp Ref Expression
1 rightssno ⊢ R ⁡ B ⊆ No
2 1 sseli ⊢ A ∈ R ⁡ B → A ∈ No