Theorem qsel

Description: If an element of a quotient set contains a given element, it is equal to the equivalence class of the element. (Contributed by Mario Carneiro, 12-Aug-2015)

	Ref	Expression
Assertion	qsel	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝐵 ∈ ( 𝐴 / 𝑅 ) ∧ 𝐶 ∈ 𝐵 ) → 𝐵 = [ 𝐶 ] 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝐴 / 𝑅 ) = ( 𝐴 / 𝑅 )
2		eleq2	⊢ ( [ 𝑥 ] 𝑅 = 𝐵 → ( 𝐶 ∈ [ 𝑥 ] 𝑅 ↔ 𝐶 ∈ 𝐵 ) )
3		eqeq1	⊢ ( [ 𝑥 ] 𝑅 = 𝐵 → ( [ 𝑥 ] 𝑅 = [ 𝐶 ] 𝑅 ↔ 𝐵 = [ 𝐶 ] 𝑅 ) )
4	2 3	imbi12d	⊢ ( [ 𝑥 ] 𝑅 = 𝐵 → ( ( 𝐶 ∈ [ 𝑥 ] 𝑅 → [ 𝑥 ] 𝑅 = [ 𝐶 ] 𝑅 ) ↔ ( 𝐶 ∈ 𝐵 → 𝐵 = [ 𝐶 ] 𝑅 ) ) )
5		elecg	⊢ ( ( 𝐶 ∈ [ 𝑥 ] 𝑅 ∧ 𝑥 ∈ V ) → ( 𝐶 ∈ [ 𝑥 ] 𝑅 ↔ 𝑥 𝑅 𝐶 ) )
6	5	elvd	⊢ ( 𝐶 ∈ [ 𝑥 ] 𝑅 → ( 𝐶 ∈ [ 𝑥 ] 𝑅 ↔ 𝑥 𝑅 𝐶 ) )
7	6	ibi	⊢ ( 𝐶 ∈ [ 𝑥 ] 𝑅 → 𝑥 𝑅 𝐶 )
8		simpll	⊢ ( ( ( 𝑅 Er 𝑋 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝐶 ) → 𝑅 Er 𝑋 )
9		simpr	⊢ ( ( ( 𝑅 Er 𝑋 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝐶 ) → 𝑥 𝑅 𝐶 )
10	8 9	erthi	⊢ ( ( ( 𝑅 Er 𝑋 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑥 𝑅 𝐶 ) → [ 𝑥 ] 𝑅 = [ 𝐶 ] 𝑅 )
11	10	ex	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑥 𝑅 𝐶 → [ 𝑥 ] 𝑅 = [ 𝐶 ] 𝑅 ) )
12	7 11	syl5	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 ∈ [ 𝑥 ] 𝑅 → [ 𝑥 ] 𝑅 = [ 𝐶 ] 𝑅 ) )
13	1 4 12	ectocld	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝐵 ∈ ( 𝐴 / 𝑅 ) ) → ( 𝐶 ∈ 𝐵 → 𝐵 = [ 𝐶 ] 𝑅 ) )
14	13	3impia	⊢ ( ( 𝑅 Er 𝑋 ∧ 𝐵 ∈ ( 𝐴 / 𝑅 ) ∧ 𝐶 ∈ 𝐵 ) → 𝐵 = [ 𝐶 ] 𝑅 )