df-qus

Description: Define a quotient ring (or quotient group), which is a special case of an image structure df-imas where the image function is x |-> [ x ] e . (Contributed by Mario Carneiro, 23-Feb-2015)

		Ref	Expression
	Assertion	df-qus	$⊢ /_{𝑠} = (r \in V, e \in V ⟼ (x \in {Base}_{r} ⟼ [x] e) “_{𝑠} r)$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cqus	$class /_{𝑠}$
1		vr	$setvar r$
2		cvv	$class V$
3		ve	$setvar e$
4		vx	$setvar x$
5		cbs	$class Base$
6	1	cv	$setvar r$
7	6 5	cfv	$class {Base}_{r}$
8	4	cv	$setvar x$
9	3	cv	$setvar e$
10	8 9	cec	$class [x] e$
11	4 7 10	cmpt	$class (x \in {Base}_{r} ⟼ [x] e)$
12		cimas	$class “_{𝑠}$
13	11 6 12	co	$class ((x \in {Base}_{r} ⟼ [x] e) “_{𝑠} r)$
14	1 3 2 2 13	cmpo	$class (r \in V, e \in V ⟼ (x \in {Base}_{r} ⟼ [x] e) “_{𝑠} r)$
15	0 14	wceq	$wff /_{𝑠} = (r \in V, e \in V ⟼ (x \in {Base}_{r} ⟼ [x] e) “_{𝑠} r)$

Metamath Proof Explorer

Definition df-qus

Detailed syntax breakdown