Definition df-frac 33153

Description: Define the field of fractions of a given integral domain. (Contributed by Thierry Arnoux, 26-Apr-2025.)

Assertion

Ref	Expression
df-frac	⊢ Frac = (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟)))

Detailed syntax breakdown of Definition df-frac

Step	Hyp	Ref	Expression
1		cfrac 33152	. 2 class Frac
2		vr	. . 3 setvar 𝑟
3		cvv 3462	. . 3 class V
4	2	cv 1533	. . . 4 class 𝑟
5		crlreg 20669	. . . . 5 class RLReg
6	4, 5	cfv 6554	. . . 4 class (RLReg‘𝑟)
7		crloc 33109	. . . 4 class RLocal
8	4, 6, 7	co 7424	. . 3 class (𝑟 RLocal (RLReg‘𝑟))
9	2, 3, 8	cmpt 5236	. 2 class (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟)))
10	1, 9	wceq 1534	1 wff Frac = (𝑟 ∈ V ↦ (𝑟 RLocal (RLReg‘𝑟)))

This definition is referenced by:  fracval  33154