Theorem ecelqsdm

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

	Ref	Expression
Assertion	ecelqsdm	$$⊢\left(\mathrm{dom}R=A\wedge \left[B\right]R\in \left(A/R\right)\right)\to B\in A$$

Proof

Step	Hyp	Ref	Expression
1		elqsn0	$$⊢\left(\mathrm{dom}R=A\wedge \left[B\right]R\in \left(A/R\right)\right)\to \left[B\right]R\ne \varnothing$$
2		ecdmn0	$$⊢B\in \mathrm{dom}R\leftrightarrow \left[B\right]R\ne \varnothing$$
3	1 2	sylibr	$$⊢\left(\mathrm{dom}R=A\wedge \left[B\right]R\in \left(A/R\right)\right)\to B\in \mathrm{dom}R$$
4		simpl	$$⊢\left(\mathrm{dom}R=A\wedge \left[B\right]R\in \left(A/R\right)\right)\to \mathrm{dom}R=A$$
5	3 4	eleqtrd	$$⊢\left(\mathrm{dom}R=A\wedge \left[B\right]R\in \left(A/R\right)\right)\to B\in A$$