Metamath Proof Explorer

Theorem bj-rveccvec

Description: Real vector spaces are subcomplex vector spaces (elemental version). (Contributed by BJ, 6-Jan-2024)

Ref Expression
Assertion bj-rveccvec 
|- ( V e. RRVec -> V e. CVec )

Proof

Step Hyp Ref Expression
1 bj-rvecsscvec 
 |-  RRVec C_ CVec
2 1 sseli 
 |-  ( V e. RRVec -> V e. CVec )