Theorem ecelqsdm

Description: Membership of an equivalence class in a quotient set. (Contributed by NM, 30-Jul-1995)

	Ref	Expression
Assertion	ecelqsdm	⊢ ( ( dom 𝑅 = 𝐴 ∧ [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ) → 𝐵 ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elqsn0	⊢ ( ( dom 𝑅 = 𝐴 ∧ [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ) → [ 𝐵 ] 𝑅 ≠ ∅ )
2		ecdmn0	⊢ ( 𝐵 ∈ dom 𝑅 ↔ [ 𝐵 ] 𝑅 ≠ ∅ )
3	1 2	sylibr	⊢ ( ( dom 𝑅 = 𝐴 ∧ [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ) → 𝐵 ∈ dom 𝑅 )
4		simpl	⊢ ( ( dom 𝑅 = 𝐴 ∧ [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ) → dom 𝑅 = 𝐴 )
5	3 4	eleqtrd	⊢ ( ( dom 𝑅 = 𝐴 ∧ [ 𝐵 ] 𝑅 ∈ ( 𝐴 / 𝑅 ) ) → 𝐵 ∈ 𝐴 )