This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0qs

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

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

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