Theorem hash0

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

	Ref	Expression
Assertion	hash0	⊢ ( ♯ ‘ ∅ ) = 0

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ∅ = ∅
2		0ex	⊢ ∅ ∈ V
3		hasheq0	⊢ ( ∅ ∈ V → ( ( ♯ ‘ ∅ ) = 0 ↔ ∅ = ∅ ) )
4	2 3	ax-mp	⊢ ( ( ♯ ‘ ∅ ) = 0 ↔ ∅ = ∅ )
5	1 4	mpbir	⊢ ( ♯ ‘ ∅ ) = 0