Theorem elqsn0

Description: A quotient set does not contain the empty set. (Contributed by NM, 24-Aug-1995)

	Ref	Expression
Assertion	elqsn0	$$⊢\left(\mathrm{dom}R=A\wedge B\in \left(A/R\right)\right)\to B\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢A/R=A/R$$
2		neeq1	$$⊢\left[x\right]R=B\to \left(\left[x\right]R\ne \varnothing \leftrightarrow B\ne \varnothing \right)$$
3		eleq2	$$⊢\mathrm{dom}R=A\to \left(x\in \mathrm{dom}R\leftrightarrow x\in A\right)$$
4	3	biimpar	$$⊢\left(\mathrm{dom}R=A\wedge x\in A\right)\to x\in \mathrm{dom}R$$
5		ecdmn0	$$⊢x\in \mathrm{dom}R\leftrightarrow \left[x\right]R\ne \varnothing$$
6	4 5	sylib	$$⊢\left(\mathrm{dom}R=A\wedge x\in A\right)\to \left[x\right]R\ne \varnothing$$
7	1 2 6	ectocld	$$⊢\left(\mathrm{dom}R=A\wedge B\in \left(A/R\right)\right)\to B\ne \varnothing$$