Definition df-2idl

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)

	Ref	Expression
Assertion	df-2idl	|- 2Ideal = ( r e. _V |-> ( ( LIdeal ` r ) i^i ( LIdeal ` ( oppR ` r ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c2idl	|- 2Ideal
1		vr	|- r
2		cvv	|- _V
3		clidl	|- LIdeal
4	1	cv	|- r
5	4 3	cfv	|- ( LIdeal ` r )
6		coppr	|- oppR
7	4 6	cfv	|- ( oppR ` r )
8	7 3	cfv	|- ( LIdeal ` ( oppR ` r ) )
9	5 8	cin	|- ( ( LIdeal ` r ) i^i ( LIdeal ` ( oppR ` r ) ) )
10	1 2 9	cmpt	|- ( r e. _V |-> ( ( LIdeal ` r ) i^i ( LIdeal ` ( oppR ` r ) ) ) )
11	0 10	wceq	|- 2Ideal = ( r e. _V |-> ( ( LIdeal ` r ) i^i ( LIdeal ` ( oppR ` r ) ) ) )