Metamath Proof Explorer

Theorem ecelqsdm

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

		Ref	Expression
	Assertion	ecelqsdm	$⊢ (dom R = A \land [B] R \in (A / R)) \to B \in A$

Step	Hyp	Ref	Expression
1		elqsn0	$⊢ (dom R = A \land [B] R \in (A / R)) \to [B] R \neq \emptyset$
2		ecdmn0	$⊢ B \in dom R \leftrightarrow [B] R \neq \emptyset$
3	1 2	sylibr	$⊢ (dom R = A \land [B] R \in (A / R)) \to B \in dom R$
4		simpl	$⊢ (dom R = A \land [B] R \in (A / R)) \to dom R = A$
5	3 4	eleqtrd	$⊢ (dom R = A \land [B] R \in (A / R)) \to B \in A$