Theorem 0qs

Description: Quotient set with the empty set. (Contributed by Peter Mazsa, 14-Sep-2019)

	Ref	Expression
Assertion	0qs	$$⊢\varnothing /R=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		df-qs	$$⊢\varnothing /R=\left\{y|\exists x\in \varnothing y=\left[x\right]R\right\}$$
2		rex0	$$⊢\neg \exists x\in \varnothing y=\left[x\right]R$$
3	2	abf	$$⊢\left\{y|\exists x\in \varnothing y=\left[x\right]R\right\}=\varnothing$$
4	1 3	eqtri	$$⊢\varnothing /R=\varnothing$$