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 ⊢ V ∈ W → V = 2 ↔ ∃ a ∃ b a ≠ b ∧ V = a b

Proof

Step Hyp Ref Expression
1 hash2prde ⊢ V ∈ W ∧ V = 2 → ∃ a ∃ b a ≠ b ∧ V = a b
2 1 ex ⊢ V ∈ W → V = 2 → ∃ a ∃ b a ≠ b ∧ V = a b
3 hashprg ⊢ a ∈ V ∧ b ∈ V → a ≠ b ↔ a b = 2
4 3 el2v ⊢ a ≠ b ↔ a b = 2
5 4 a1i ⊢ V = a b → a ≠ b ↔ a b = 2
6 5 biimpd ⊢ V = a b → a ≠ b → a b = 2
7 fveqeq2 ⊢ V = a b → V = 2 ↔ a b = 2
8 6 7 sylibrd ⊢ V = a b → a ≠ b → V = 2
9 8 impcom ⊢ a ≠ b ∧ V = a b → V = 2
10 9 a1i ⊢ V ∈ W → a ≠ b ∧ V = a b → V = 2
11 10 exlimdvv ⊢ V ∈ W → ∃ a ∃ b a ≠ b ∧ V = a b → V = 2
12 2 11 impbid ⊢ V ∈ W → V = 2 ↔ ∃ a ∃ b a ≠ b ∧ V = a b