Metamath Proof Explorer

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