Theorem rimval

Description: The set of ring isomorphisms. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by AV, 24-Jul-2026)

	Ref	Expression
Hypotheses	rhmf1o.b	$$⊢B={\mathrm{Base}}_R$$
	rhmf1o.c	$$⊢C={\mathrm{Base}}_S$$
Assertion	rimval	$$⊢R\mathrm{RingIso}S=\left\{f\in \left(R\mathrm{RingHom}S\right)|f:B\underset{1-1\; onto}{⟶}C\right\}$$

Proof

Step	Hyp	Ref	Expression
1		rhmf1o.b	$$⊢B={\mathrm{Base}}_R$$
2		rhmf1o.c	$$⊢C={\mathrm{Base}}_S$$
3	1 2	isrim	$$⊢x\in \left(R\mathrm{RingIso}S\right)\leftrightarrow \left(x\in \left(R\mathrm{RingHom}S\right)\wedge x:B\underset{1-1\; onto}{⟶}C\right)$$
4		f1oeq1	$$⊢f=x\to \left(f:B\underset{1-1\; onto}{⟶}C\leftrightarrow x:B\underset{1-1\; onto}{⟶}C\right)$$
5	4	elrab	$$⊢x\in \left\{f\in \left(R\mathrm{RingHom}S\right)|f:B\underset{1-1\; onto}{⟶}C\right\}\leftrightarrow \left(x\in \left(R\mathrm{RingHom}S\right)\wedge x:B\underset{1-1\; onto}{⟶}C\right)$$
6	3 5	bitr4i	$$⊢x\in \left(R\mathrm{RingIso}S\right)\leftrightarrow x\in \left\{f\in \left(R\mathrm{RingHom}S\right)|f:B\underset{1-1\; onto}{⟶}C\right\}$$
7	6	eqriv	$$⊢R\mathrm{RingIso}S=\left\{f\in \left(R\mathrm{RingHom}S\right)|f:B\underset{1-1\; onto}{⟶}C\right\}$$