Metamath Proof Explorer


Definition df-zrng

Description: Define the subring of integral elements in a ring. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Assertion df-zrng ℤRing = r V r IntgRing ran ℤRHom r

Detailed syntax breakdown

Step Hyp Ref Expression
0 czr class ℤRing
1 vr setvar r
2 cvv class V
3 1 cv setvar r
4 citr class IntgRing
5 czrh class ℤRHom
6 3 5 cfv class ℤRHom r
7 6 crn class ran ℤRHom r
8 3 7 4 co class r IntgRing ran ℤRHom r
9 1 2 8 cmpt class r V r IntgRing ran ℤRHom r
10 0 9 wceq wff ℤRing = r V r IntgRing ran ℤRHom r