Definition df-ric 20794

Description: Define the ring isomorphism relation, analogous to df-gic 19524: Two (unital) rings are said to be isomorphic iff they are connected by at least one isomorphism. Isomorphic rings share all global ring properties, but to relate local properties requires knowledge of a specific isomorphism. (Contributed by Jeff Madsen, 16-Jun-2011.) Adapted to df-gic 19524. (Revised by AV, 24-Dec-2019.)

Assertion

Ref	Expression
df-ric	⊢ ≃𝑟 = (◡ RingIso “ (V ∖ 1o))

Detailed syntax breakdown of Definition df-ric

Step	Hyp	Ref	Expression
1		cric 20752	. 2 class ≃𝑟
2		crs 20751	. . . 4 class RingIso
3	2	ccnv 5657	. . 3 class ◡ RingIso
4		cvv 3454	. . . 4 class V
5		c1o 8507	. . . 4 class 1o
6	4, 5	cdif 4048	. . 3 class (V ∖ 1o)
7	3, 6	cima 5661	. 2 class (◡ RingIso “ (V ∖ 1o))
8	1, 7	wceq 1570	1 wff ≃𝑟 = (◡ RingIso “ (V ∖ 1o))

This definition is used by:  ricrel  20795  brric  20796