Definition df-2idl 16258

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 = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )

Detailed syntax breakdown of Definition df-2idl

Step	Hyp	Ref	Expression
1		c2idl 16257	. 2 class 2Ideal
2		vr	. . 3 set r
3		cvv 2916	. . 3 class _V
4	2	cv 1648	. . . . 5 class r
5		clidl 16197	. . . . 5 class LIdeal
6	4, 5	cfv 5413	. . . 4 class (LIdeal ` r )
7		coppr 15682	. . . . . 6 class oppr
8	4, 7	cfv 5413	. . . . 5 class (oppr ` r )
9	8, 5	cfv 5413	. . . 4 class (LIdeal ` (oppr ` r ) )
10	6, 9	cin 3279	. . 3 class ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) )
11	2, 3, 10	cmpt 4226	. 2 class ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
12	1, 11	wceq 1649	1 wff 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )

This definition is referenced by:  2idlval  16259