This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-qs

Description: Define quotient set. R is usually an equivalence relation. Definition of Enderton p. 58. (Contributed by NM, 23-Jul-1995)

		Ref	Expression
	Assertion	df-qs	$⊢ A / R = \{y \| \exists x \in A y = [x] R\}$

Step	Hyp	Ref	Expression
0		cA	$class A$
1		cR	$class R$
2	0 1	cqs	$class (A / R)$
3		vy	$setvar y$
4		vx	$setvar x$
5	3	cv	$setvar y$
6	4	cv	$setvar x$
7	6 1	cec	$class [x] R$
8	5 7	wceq	$wff y = [x] R$
9	8 4 0	wrex	$wff \exists x \in A y = [x] R$
10	9 3	cab	$class \{y \| \exists x \in A y = [x] R\}$
11	2 10	wceq	$wff A / R = \{y \| \exists x \in A y = [x] R\}$