Theorem hash0

Description: The empty set has size zero. (Contributed by Mario Carneiro, 8-Jul-2014)

	Ref	Expression
Assertion	hash0	$$⊢\left|\varnothing \right|=0$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\varnothing =\varnothing$$
2		0ex	$$⊢\varnothing \in \mathrm{V}$$
3		hasheq0	$$⊢\varnothing \in \mathrm{V}\to \left(\left|\varnothing \right|=0\leftrightarrow \varnothing =\varnothing \right)$$
4	2 3	ax-mp	$$⊢\left|\varnothing \right|=0\leftrightarrow \varnothing =\varnothing$$
5	1 4	mpbir	$$⊢\left|\varnothing \right|=0$$