Definition 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	|- /s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cqus	|- /s
1		vr	|- r
2		cvv	|- _V
3		ve	|- e
4		vx	|- x
5		cbs	|- Base
6	1	cv	|- r
7	6 5	cfv	|- ( Base ` r )
8	4	cv	|- x
9	3	cv	|- e
10	8 9	cec	|- [ x ] e
11	4 7 10	cmpt	|- ( x e. ( Base ` r ) |-> [ x ] e )
12		cimas	|- "s
13	11 6 12	co	|- ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r )
14	1 3 2 2 13	cmpo	|- ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
15	0 14	wceq	|- /s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )