Metamath Proof Explorer


Theorem zssq

Description: The integers are a subset of the rationals. (Contributed by NM, 9-Jan-2002)

Ref Expression
Assertion zssq ⊢ ℤ ⊆ ℚ

Proof

Step Hyp Ref Expression
1 zq ⊢ x ∈ ℤ → x ∈ ℚ
2 1 ssriv ⊢ ℤ ⊆ ℚ