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 \in V ⟼ LIdeal (r) \cap LIdeal ({opp}_{r} (r)))$

Detailed syntax breakdown

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

Metamath Proof Explorer

Definition df-2idl

Detailed syntax breakdown