Metamath Proof Explorer


Theorem isnzr

Description: Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015)

Ref Expression
Hypotheses isnzr.o 1 ˙ = 1 R
isnzr.z 0 ˙ = 0 R
Assertion isnzr R NzRing R Ring 1 ˙ 0 ˙

Proof

Step Hyp Ref Expression
1 isnzr.o 1 ˙ = 1 R
2 isnzr.z 0 ˙ = 0 R
3 fveq2 r = R 1 r = 1 R
4 3 1 eqtr4di r = R 1 r = 1 ˙
5 fveq2 r = R 0 r = 0 R
6 5 2 eqtr4di r = R 0 r = 0 ˙
7 4 6 neeq12d r = R 1 r 0 r 1 ˙ 0 ˙
8 df-nzr NzRing = r Ring | 1 r 0 r
9 7 8 elrab2 R NzRing R Ring 1 ˙ 0 ˙