Definition df-2idl 20416

Description: Define the class of two-sided ideals of a ring. A two-sided ideal is a left ideal which is also a right ideal (or a left ideal over the opposite ring). (Contributed by Mario Carneiro, 14-Jun-2015.)

Assertion

Ref	Expression
df-2idl	⊢ 2Ideal = (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr‘𝑟))))

Detailed syntax breakdown of Definition df-2idl

Step	Hyp	Ref	Expression
1		c2idl 20415	. 2 class 2Ideal
2		vr	. . 3 setvar 𝑟
3		cvv 3422	. . 3 class V
4	2	cv 1538	. . . . 5 class 𝑟
5		clidl 20347	. . . . 5 class LIdeal
6	4, 5	cfv 6418	. . . 4 class (LIdeal‘𝑟)
7		coppr 19776	. . . . . 6 class oppr
8	4, 7	cfv 6418	. . . . 5 class (oppr‘𝑟)
9	8, 5	cfv 6418	. . . 4 class (LIdeal‘(oppr‘𝑟))
10	6, 9	cin 3882	. . 3 class ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr‘𝑟)))
11	2, 3, 10	cmpt 5153	. 2 class (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr‘𝑟))))
12	1, 11	wceq 1539	1 wff 2Ideal = (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr‘𝑟))))

This definition is referenced by:  2idlval  20417