Metamath Proof Explorer

Theorem subrgccsscc

Description: A subring of the complex numbers is a subset of the complex numbers. (Contributed by AV, 26-Oct-2026)

Ref Expression
Assertion subrgccsscc 
|- ( S e. ( SubRing ` CCfld ) -> S C_ CC )

Proof

Step Hyp Ref Expression
1 cnfldbas 
 |-  CC = ( Base ` CCfld )
2 1 subrgss 
 |-  ( S e. ( SubRing ` CCfld ) -> S C_ CC )