Theorem eqvrelqsel

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) (Revised by Peter Mazsa, 28-Dec-2019)

	Ref	Expression
Assertion	eqvrelqsel	⊢ ( ( EqvRel 𝑅 ∧ 𝐵 ∈ ( 𝐴 / 𝑅 ) ∧ 𝐶 ∈ 𝐵 ) → 𝐵 = [ 𝐶 ] 𝑅 )

Proof

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