Theorem pr0hash2ex

Description: There is (at least) one set with two different elements: the unordered pair containing the empty set and the singleton containing the empty set. (Contributed by AV, 29-Jan-2020)

	Ref	Expression
Assertion	pr0hash2ex	⊢ ( ♯ ‘ { ∅ , { ∅ } } ) = 2

Proof

Step	Hyp	Ref	Expression
1		df2o2	⊢ 2o = { ∅ , { ∅ } }
2	1	eqcomi	⊢ { ∅ , { ∅ } } = 2o
3	2	fveq2i	⊢ ( ♯ ‘ { ∅ , { ∅ } } ) = ( ♯ ‘ 2o )
4		hash2	⊢ ( ♯ ‘ 2o ) = 2
5	3 4	eqtri	⊢ ( ♯ ‘ { ∅ , { ∅ } } ) = 2