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

Metamath Proof Explorer

Theorem hash2exprb

Description: A set of size two is an unordered pair if and only if it contains two different elements. (Contributed by Alexander van der Vekens, 14-Jan-2018)

Ref Expression
Assertion hash2exprb ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 2 ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )

Proof

Step Hyp Ref Expression
1 hash2prde ⊢ ( ( 𝑉 ∈ 𝑊 ∧ ( ♯ ‘ 𝑉 ) = 2 ) → ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) )
2 1 ex ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 2 → ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )
3 hashprg ⊢ ( ( 𝑎 ∈ V ∧ 𝑏 ∈ V ) → ( 𝑎 ≠ 𝑏 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
4 3 el2v ⊢ ( 𝑎 ≠ 𝑏 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 )
5 4 a1i ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑎 ≠ 𝑏 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
6 5 biimpd ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑎 ≠ 𝑏 → ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
7 fveqeq2 ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( ( ♯ ‘ 𝑉 ) = 2 ↔ ( ♯ ‘ { 𝑎 , 𝑏 } ) = 2 ) )
8 6 7 sylibrd ⊢ ( 𝑉 = { 𝑎 , 𝑏 } → ( 𝑎 ≠ 𝑏 → ( ♯ ‘ 𝑉 ) = 2 ) )
9 8 impcom ⊢ ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( ♯ ‘ 𝑉 ) = 2 )
10 9 a1i ⊢ ( 𝑉 ∈ 𝑊 → ( ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( ♯ ‘ 𝑉 ) = 2 ) )
11 10 exlimdvv ⊢ ( 𝑉 ∈ 𝑊 → ( ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) → ( ♯ ‘ 𝑉 ) = 2 ) )
12 2 11 impbid ⊢ ( 𝑉 ∈ 𝑊 → ( ( ♯ ‘ 𝑉 ) = 2 ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )