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	$$⊢\mathrm{2Ideal}=\left(r\in \mathrm{V}⟼\mathrm{LIdeal}\left(r\right)\cap \mathrm{LIdeal}\left({opp}_r\left(r\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c2idl	$$class\mathrm{2Ideal}$$
1		vr	$$setvarr$$
2		cvv	$$class\mathrm{V}$$
3		clidl	$$class\mathrm{LIdeal}$$
4	1	cv	$$setvarr$$
5	4 3	cfv	$$class\mathrm{LIdeal}\left(r\right)$$
6		coppr	$$class{opp}_r$$
7	4 6	cfv	$$class{opp}_r\left(r\right)$$
8	7 3	cfv	$$class\mathrm{LIdeal}\left({opp}_r\left(r\right)\right)$$
9	5 8	cin	$$class\left(\mathrm{LIdeal}\left(r\right)\cap \mathrm{LIdeal}\left({opp}_r\left(r\right)\right)\right)$$
10	1 2 9	cmpt	$$class\left(r\in \mathrm{V}⟼\mathrm{LIdeal}\left(r\right)\cap \mathrm{LIdeal}\left({opp}_r\left(r\right)\right)\right)$$
11	0 10	wceq	$$wff\mathrm{2Ideal}=\left(r\in \mathrm{V}⟼\mathrm{LIdeal}\left(r\right)\cap \mathrm{LIdeal}\left({opp}_r\left(r\right)\right)\right)$$