Definition df-risc 33782

Description: Define the ring isomorphism relation. (Contributed by Jeff Madsen, 16-Jun-2011.)

Assertion

Ref	Expression
df-risc	|- ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) }

Distinct variable group:   s, r, f

Detailed syntax breakdown of Definition df-risc

Step	Hyp	Ref	Expression
1		crisc 33761	. 2 class ~=R
2		vr	. . . . . . 7 setvar r
3	2	cv 1482	. . . . . 6 class r
4		crngo 33693	. . . . . 6 class RingOps
5	3, 4	wcel 1990	. . . . 5 wff r e. RingOps
6		vs	. . . . . . 7 setvar s
7	6	cv 1482	. . . . . 6 class s
8	7, 4	wcel 1990	. . . . 5 wff s e. RingOps
9	5, 8	wa 384	. . . 4 wff ( r e. RingOps /\ s e. RingOps )
10		vf	. . . . . . 7 setvar f
11	10	cv 1482	. . . . . 6 class f
12		crngiso 33760	. . . . . . 7 class RngIso
13	3, 7, 12	co 6650	. . . . . 6 class ( r RngIso s )
14	11, 13	wcel 1990	. . . . 5 wff f e. ( r RngIso s )
15	14, 10	wex 1704	. . . 4 wff E. f f e. ( r RngIso s )
16	9, 15	wa 384	. . 3 wff ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) )
17	16, 2, 6	copab 4712	. 2 class { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) }
18	1, 17	wceq 1483	1 wff ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) }

This definition is referenced by:  isriscg  33783  riscer  33787