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	$$⊢\left|\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right|=2$$

Proof

Step	Hyp	Ref	Expression
1		df2o2	$$⊢2_{𝑜}=\left\{\varnothing ,\left\{\varnothing \right\}\right\}$$
2	1	eqcomi	$$⊢\left\{\varnothing ,\left\{\varnothing \right\}\right\}=2_{𝑜}$$
3	2	fveq2i	$$⊢\left|\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right|=\left|2_{𝑜}\right|$$
4		hash2	$$⊢\left|2_{𝑜}\right|=2$$
5	3 4	eqtri	$$⊢\left|\left\{\varnothing ,\left\{\varnothing \right\}\right\}\right|=2$$