Metamath Proof Explorer

Theorem qssaa

Description: The rational numbers are contained in the algebraic numbers. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Assertion qssaa 
|- QQ C_ AA

Proof

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