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