This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem zssq

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

Ref Expression
Assertion zssq 
|- ZZ C_ QQ

Proof

Step Hyp Ref Expression
1 zq 
 |-  ( x e. ZZ -> x e. QQ )
2 1 ssriv 
 |-  ZZ C_ QQ