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 ↔ ∃ 𝑎 ∃ 𝑏 ( 𝑎 ≠ 𝑏 ∧ 𝑉 = { 𝑎 , 𝑏 } ) ) )