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	⊢ ( 𝐴 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 }

Step	Hyp	Ref	Expression
0		cA	⊢ 𝐴
1		cR	⊢ 𝑅
2	0 1	cqs	⊢ ( 𝐴 / 𝑅 )
3		vy	⊢ 𝑦
4		vx	⊢ 𝑥
5	3	cv	⊢ 𝑦
6	4	cv	⊢ 𝑥
7	6 1	cec	⊢ [ 𝑥 ] 𝑅
8	5 7	wceq	⊢ 𝑦 = [ 𝑥 ] 𝑅
9	8 4 0	wrex	⊢ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅
10	9 3	cab	⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 }
11	2 10	wceq	⊢ ( 𝐴 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 }