This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ℤ = ( Base ‘ ℤring )

Proof

Step Hyp Ref Expression
1 zsscn ⊢ ℤ ⊆ ℂ
2 df-zring ⊢ ℤring = ( ℂfld ↾s ℤ )
3 cnfldbas ⊢ ℂ = ( Base ‘ ℂfld )
4 2 3 ressbas2 ⊢ ( ℤ ⊆ ℂ → ℤ = ( Base ‘ ℤring ) )
5 1 4 ax-mp ⊢ ℤ = ( Base ‘ ℤring )