Definition df-risc

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

	Ref	Expression
Assertion	df-risc	Could not format assertion : No typesetting found for |- ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) } with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		crisc	$$class{\simeq }_{𝑟}$$
1		vr	$$setvarr$$
2		vs	$$setvars$$
3	1	cv	$$setvarr$$
4		crngo	$$class\mathrm{RingOps}$$
5	3 4	wcel	$$wffr\in \mathrm{RingOps}$$
6	2	cv	$$setvars$$
7	6 4	wcel	$$wffs\in \mathrm{RingOps}$$
8	5 7	wa	$$wff\left(r\in \mathrm{RingOps}\wedge s\in \mathrm{RingOps}\right)$$
9		vf	$$setvarf$$
10	9	cv	$$setvarf$$
11		crngoiso	Could not format RingOpsIso : No typesetting found for class RingOpsIso with typecode class
12	3 6 11	co	Could not format ( r RingOpsIso s ) : No typesetting found for class ( r RingOpsIso s ) with typecode class
13	10 12	wcel	Could not format f e. ( r RingOpsIso s ) : No typesetting found for wff f e. ( r RingOpsIso s ) with typecode wff
14	13 9	wex	Could not format E. f f e. ( r RingOpsIso s ) : No typesetting found for wff E. f f e. ( r RingOpsIso s ) with typecode wff
15	8 14	wa	Could not format ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) : No typesetting found for wff ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) with typecode wff
16	15 1 2	copab	Could not format { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) } : No typesetting found for class { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) } with typecode class
17	0 16	wceq	Could not format ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) } : No typesetting found for wff ~=R = { <. r , s >. | ( ( r e. RingOps /\ s e. RingOps ) /\ E. f f e. ( r RingOpsIso s ) ) } with typecode wff