Metamath Proof Explorer


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 𝑟
1 vr setvar r
2 vs setvar s
3 1 cv setvar r
4 crngo class RingOps
5 3 4 wcel wff r RingOps
6 2 cv setvar s
7 6 4 wcel wff s RingOps
8 5 7 wa wff r RingOps s RingOps
9 vf setvar f
10 9 cv setvar f
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