This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem prhash2ex

Description: There is (at least) one set with two different elements: the unordered pair containing 0 and 1 . In contrast to pr0hash2ex , numbers are used instead of sets because their representation is shorter (and more comprehensive). (Contributed by AV, 29-Jan-2020)

Ref Expression
Assertion prhash2ex ⊢ 0 1 = 2

Proof

Step Hyp Ref Expression
1 0ne1 ⊢ 0 ≠ 1
2 c0ex ⊢ 0 ∈ V
3 1ex ⊢ 1 ∈ V
4 hashprg ⊢ 0 ∈ V ∧ 1 ∈ V → 0 ≠ 1 ↔ 0 1 = 2
5 4 bicomd ⊢ 0 ∈ V ∧ 1 ∈ V → 0 1 = 2 ↔ 0 ≠ 1
6 2 3 5 mp2an ⊢ 0 1 = 2 ↔ 0 ≠ 1
7 1 6 mpbir ⊢ 0 1 = 2