Metamath Proof Explorer

Theorem aasscn

Description: The algebraic numbers are a subset of the complex numbers. (Contributed by Mario Carneiro, 23-Jul-2014)

Ref Expression
Assertion aasscn 
|- AA C_ CC

Proof

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