Definition df-ric 20362

Description: Define the ring isomorphism relation, analogous to df-gic 19170: 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 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 20358	. 2 class ≃𝑟
2		crs 20357	. . . 4 class RingIso
3	2	ccnv 5665	. . 3 class ◡ RingIso
4		cvv 3466	. . . 4 class V
5		c1o 8454	. . . 4 class 1o
6	4, 5	cdif 3937	. . 3 class (V ∖ 1o)
7	3, 6	cima 5669	. 2 class (◡ RingIso “ (V ∖ 1o))
8	1, 7	wceq 1533	1 wff ≃𝑟 = (◡ RingIso “ (V ∖ 1o))

This definition is referenced by:  brric  20391