Metamath Proof Explorer

Theorem zringbas

Description: The integers are the base of the ring of integers. (Contributed by Thierry Arnoux, 31-Oct-2017) (Revised by AV, 9-Jun-2019)

Ref Expression
Assertion zringbas 
|- ZZ = ( Base ` ZZring )

Proof

Step Hyp Ref Expression
1 zsscn 
 |-  ZZ C_ CC
2 df-zring 
 |-  ZZring = ( CCfld |`s ZZ )
3 cnfldbas 
 |-  CC = ( Base ` CCfld )
4 2 3 ressbas2 
 |-  ( ZZ C_ CC -> ZZ = ( Base ` ZZring ) )
5 1 4 ax-mp 
 |-  ZZ = ( Base ` ZZring )