n0elqs

Description: Two ways of expressing that the empty set is not an element of a quotient set. (Contributed by Peter Mazsa, 5-Dec-2019)

		Ref	Expression
	Assertion	n0elqs	$⊢ \neg \emptyset \in (A / R) \leftrightarrow A \subseteq dom R$

Step	Hyp	Ref	Expression
1		ecdmn0	$⊢ x \in dom R \leftrightarrow [x] R \neq \emptyset$
2	1	ralbii	$⊢ \forall x \in A x \in dom R \leftrightarrow \forall x \in A [x] R \neq \emptyset$
3		dfss3	$⊢ A \subseteq dom R \leftrightarrow \forall x \in A x \in dom R$
4		nne	$⊢ \neg [x] R \neq \emptyset \leftrightarrow [x] R = \emptyset$
5	4	rexbii	$⊢ \exists x \in A \neg [x] R \neq \emptyset \leftrightarrow \exists x \in A [x] R = \emptyset$
6	5	notbii	$⊢ \neg \exists x \in A \neg [x] R \neq \emptyset \leftrightarrow \neg \exists x \in A [x] R = \emptyset$
7		dfral2	$⊢ \forall x \in A [x] R \neq \emptyset \leftrightarrow \neg \exists x \in A \neg [x] R \neq \emptyset$
8		0ex	$⊢ \emptyset \in V$
9	8	elqs	$⊢ \emptyset \in (A / R) \leftrightarrow \exists x \in A \emptyset = [x] R$
10		eqcom	$⊢ \emptyset = [x] R \leftrightarrow [x] R = \emptyset$
11	10	rexbii	$⊢ \exists x \in A \emptyset = [x] R \leftrightarrow \exists x \in A [x] R = \emptyset$
12	9 11	bitri	$⊢ \emptyset \in (A / R) \leftrightarrow \exists x \in A [x] R = \emptyset$
13	12	notbii	$⊢ \neg \emptyset \in (A / R) \leftrightarrow \neg \exists x \in A [x] R = \emptyset$
14	6 7 13	3bitr4ri	$⊢ \neg \emptyset \in (A / R) \leftrightarrow \forall x \in A [x] R \neq \emptyset$
15	2 3 14	3bitr4ri	$⊢ \neg \emptyset \in (A / R) \leftrightarrow A \subseteq dom R$

Metamath Proof Explorer