Metamath Proof Explorer


Theorem cnfldsrngbas

Description: The base set of a subring of the field of complex numbers. (Contributed by AV, 31-Jan-2020)

Ref Expression
Hypothesis cnfldsrngbas.r 𝑅 = ( ℂflds 𝑆 )
Assertion cnfldsrngbas ( 𝑆 ⊆ ℂ → 𝑆 = ( Base ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 cnfldsrngbas.r 𝑅 = ( ℂflds 𝑆 )
2 cnfldbas ℂ = ( Base ‘ ℂfld )
3 1 2 ressbas2 ( 𝑆 ⊆ ℂ → 𝑆 = ( Base ‘ 𝑅 ) )