hash1n0

Description: If the size of a set is 1 the set is not empty. (Contributed by AV, 23-Dec-2020)

		Ref	Expression
	Assertion	hash1n0	$⊢ (A \in V \land \|A\| = 1) \to A \neq \emptyset$

Step	Hyp	Ref	Expression
1		hash1snb	$⊢ A \in V \to (\|A\| = 1 \leftrightarrow \exists a A = \{a\})$
2		id	$⊢ A = \{a\} \to A = \{a\}$
3		vex	$⊢ a \in V$
4	3	snnz	$⊢ \{a\} \neq \emptyset$
5	4	a1i	$⊢ A = \{a\} \to \{a\} \neq \emptyset$
6	2 5	eqnetrd	$⊢ A = \{a\} \to A \neq \emptyset$
7	6	exlimiv	$⊢ \exists a A = \{a\} \to A \neq \emptyset$
8	1 7	biimtrdi	$⊢ A \in V \to (\|A\| = 1 \to A \neq \emptyset)$
9	8	imp	$⊢ (A \in V \land \|A\| = 1) \to A \neq \emptyset$

Metamath Proof Explorer