Metamath Proof Explorer


Theorem qssre

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

Ref Expression
Assertion qssre ⊢ ℚ ⊆ ℝ

Proof

Step Hyp Ref Expression
1 qre ⊢ x ∈ ℚ → x ∈ ℝ
2 1 ssriv ⊢ ℚ ⊆ ℝ