Theorem ecelqsg

Description: Membership of an equivalence class in a quotient set. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 9-Jul-2014)

	Ref	Expression
Assertion	ecelqsg	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴 ) → [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ [ 𝐵 ] 𝑅 = [ 𝐵 ] 𝑅
2		eceq1	⊢ ( 𝑥 = 𝐵 → [ 𝑥 ] 𝑅 = [ 𝐵 ] 𝑅 )
3	2	rspceeqv	⊢ ( ( 𝐵 ∈ 𝐴 ∧ [ 𝐵 ] 𝑅 = [ 𝐵 ] 𝑅 ) → ∃ 𝑥 ∈ 𝐴 [ 𝐵 ] 𝑅 = [ 𝑥 ] 𝑅 )
4	1 3	mpan2	⊢ ( 𝐵 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 [ 𝐵 ] 𝑅 = [ 𝑥 ] 𝑅 )
5		ecexg	⊢ ( 𝑅 ∈ 𝑉 → [ 𝐵 ] 𝑅 ∈ V )
6		elqsg	⊢ ( [ 𝐵 ] 𝑅 ∈ V → ( [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐴 [ 𝐵 ] 𝑅 = [ 𝑥 ] 𝑅 ) )
7	5 6	syl	⊢ ( 𝑅 ∈ 𝑉 → ( [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ↔ ∃ 𝑥 ∈ 𝐴 [ 𝐵 ] 𝑅 = [ 𝑥 ] 𝑅 ) )
8	7	biimpar	⊢ ( ( 𝑅 ∈ 𝑉 ∧ ∃ 𝑥 ∈ 𝐴 [ 𝐵 ] 𝑅 = [ 𝑥 ] 𝑅 ) → [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )
9	4 8	sylan2	⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐵 ∈ 𝐴 ) → [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) )