Metamath Proof Explorer


Theorem zno

Description: A surreal integer is a surreal. (Contributed by Scott Fenton, 17-May-2025)

Ref Expression
Assertion zno ( 𝐴 ∈ ℤs → 𝐴 ∈ No )

Proof

Step Hyp Ref Expression
1 zssno ⊢ ℤs ⊆ No
2 1 sseli ⊢ ( 𝐴 ∈ ℤs → 𝐴 ∈ No )