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

Metamath Proof Explorer

Theorem ecelqs

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

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

Proof

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