Theorem nzrring

Description: A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015) (Proof shortened by SN, 23-Feb-2025)

	Ref	Expression
Assertion	nzrring	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )

Proof

Step	Hyp	Ref	Expression
1		df-nzr	⊢ NzRing = { 𝑟 ∈ Ring ∣ ( 1r ‘ 𝑟 ) ≠ ( 0g ‘ 𝑟 ) }
2	1	ssrab3	⊢ NzRing ⊆ Ring
3	2	sseli	⊢ ( 𝑅 ∈ NzRing → 𝑅 ∈ Ring )