Metamath Proof Explorer


Definition df-rngiso

Description: Define the set of ring isomorphisms from r to s . (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Assertion df-rngiso RingIso=rV,sVfrRingHoms|f-1sRingHomr

Detailed syntax breakdown

Step Hyp Ref Expression
0 crs classRingIso
1 vr setvarr
2 cvv classV
3 vs setvars
4 vf setvarf
5 1 cv setvarr
6 crh classRingHom
7 3 cv setvars
8 5 7 6 co classrRingHoms
9 4 cv setvarf
10 9 ccnv classf-1
11 7 5 6 co classsRingHomr
12 10 11 wcel wfff-1sRingHomr
13 12 4 8 crab classfrRingHoms|f-1sRingHomr
14 1 3 2 2 13 cmpo classrV,sVfrRingHoms|f-1sRingHomr
15 0 14 wceq wffRingIso=rV,sVfrRingHoms|f-1sRingHomr