Theorem 0ring01eqbi2

Description: In a ring, 0 = 1 iff the ring contains only 0 . (Contributed by Jeff Madsen, 6-Jan-2011) (Revised by AV, 27-Jun-2026)

	Ref	Expression
Hypotheses	0ring.b	$$⊢B={\mathrm{Base}}_R$$
	0ring.0	$$⊢\underset{\dot{}}{0}=0_R$$
	0ring01eq.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	0ring01eqbi2	$$⊢R\in \mathrm{Ring}\to \left(B=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$

Proof

Step	Hyp	Ref	Expression
1		0ring.b	$$⊢B={\mathrm{Base}}_R$$
2		0ring.0	$$⊢\underset{\dot{}}{0}=0_R$$
3		0ring01eq.1	$$⊢\underset{\dot{}}{1}=1_R$$
4		fveq2	$$⊢B=\left\{\underset{\dot{}}{0}\right\}\to \left|B\right|=\left|\left\{\underset{\dot{}}{0}\right\}\right|$$
5	2	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
6		hashsng	$$⊢\underset{\dot{}}{0}\in \mathrm{V}\to \left|\left\{\underset{\dot{}}{0}\right\}\right|=1$$
7	5 6	ax-mp	$$⊢\left|\left\{\underset{\dot{}}{0}\right\}\right|=1$$
8	4 7	eqtrdi	$$⊢B=\left\{\underset{\dot{}}{0}\right\}\to \left|B\right|=1$$
9	1 2 3	0ring01eq	$$⊢\left(R\in \mathrm{Ring}\wedge \left|B\right|=1\right)\to \underset{\dot{}}{0}=\underset{\dot{}}{1}$$
10	8 9	sylan2	$$⊢\left(R\in \mathrm{Ring}\wedge B=\left\{\underset{\dot{}}{0}\right\}\right)\to \underset{\dot{}}{0}=\underset{\dot{}}{1}$$
11	10	eqcomd	$$⊢\left(R\in \mathrm{Ring}\wedge B=\left\{\underset{\dot{}}{0}\right\}\right)\to \underset{\dot{}}{1}=\underset{\dot{}}{0}$$
12	11	ex	$$⊢R\in \mathrm{Ring}\to \left(B=\left\{\underset{\dot{}}{0}\right\}\to \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$
13		eqcom	$$⊢\underset{\dot{}}{1}=\underset{\dot{}}{0}\leftrightarrow \underset{\dot{}}{0}=\underset{\dot{}}{1}$$
14	1 2 3	01eq0ring	$$⊢\left(R\in \mathrm{Ring}\wedge \underset{\dot{}}{0}=\underset{\dot{}}{1}\right)\to B=\left\{\underset{\dot{}}{0}\right\}$$
15	14	ex	$$⊢R\in \mathrm{Ring}\to \left(\underset{\dot{}}{0}=\underset{\dot{}}{1}\to B=\left\{\underset{\dot{}}{0}\right\}\right)$$
16	13 15	biimtrid	$$⊢R\in \mathrm{Ring}\to \left(\underset{\dot{}}{1}=\underset{\dot{}}{0}\to B=\left\{\underset{\dot{}}{0}\right\}\right)$$
17	12 16	impbid	$$⊢R\in \mathrm{Ring}\to \left(B=\left\{\underset{\dot{}}{0}\right\}\leftrightarrow \underset{\dot{}}{1}=\underset{\dot{}}{0}\right)$$