Definition df-risc

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crisc	|- ~=R
1		vr	|- r
2		vs	|- s
3	1	cv	|- r
4		crngo	|- RingOps
5	3 4	wcel	|- r e. RingOps
6	2	cv	|- s
7	6 4	wcel	|- s e. RingOps
8	5 7	wa	|- ( r e. RingOps /\ s e. RingOps )
9		vf	|- f
10	9	cv	|- f
11		crngiso	|- RngIso
12	3 6 11	co	|- ( r RngIso s )
13	10 12	wcel	|- f e. ( r RngIso s )
14	13 9	wex	|- E. f f e. ( r RngIso s )
15	8 14	wa	|- ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) )
16	15 1 2	copab	|- { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) }
17	0 16	wceq	|- ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RngIso s ) ) }