Theorem 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	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) = 1 ) → 𝐴 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		hash1snb	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 1 ↔ ∃ 𝑎 𝐴 = { 𝑎 } ) )
2		id	⊢ ( 𝐴 = { 𝑎 } → 𝐴 = { 𝑎 } )
3		vex	⊢ 𝑎 ∈ V
4	3	snnz	⊢ { 𝑎 } ≠ ∅
5	4	a1i	⊢ ( 𝐴 = { 𝑎 } → { 𝑎 } ≠ ∅ )
6	2 5	eqnetrd	⊢ ( 𝐴 = { 𝑎 } → 𝐴 ≠ ∅ )
7	6	exlimiv	⊢ ( ∃ 𝑎 𝐴 = { 𝑎 } → 𝐴 ≠ ∅ )
8	1 7	biimtrdi	⊢ ( 𝐴 ∈ 𝑉 → ( ( ♯ ‘ 𝐴 ) = 1 → 𝐴 ≠ ∅ ) )
9	8	imp	⊢ ( ( 𝐴 ∈ 𝑉 ∧ ( ♯ ‘ 𝐴 ) = 1 ) → 𝐴 ≠ ∅ )