Metamath Proof Explorer

Theorem hash2prb

Description: A set of size two is a proper unordered pair. (Contributed by AV, 1-Nov-2020)

Ref Expression
Assertion hash2prb ⊢ V ∈ W → V = 2 ↔ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ V = a b

Proof

Step Hyp Ref Expression
1 hash2exprb ⊢ V ∈ W → V = 2 ↔ ∃ a ∃ b a ≠ b ∧ V = a b
2 vex ⊢ a ∈ V
3 2 prid1 ⊢ a ∈ a b
4 vex ⊢ b ∈ V
5 4 prid2 ⊢ b ∈ a b
6 3 5 pm3.2i ⊢ a ∈ a b ∧ b ∈ a b
7 eleq2 ⊢ V = a b → a ∈ V ↔ a ∈ a b
8 eleq2 ⊢ V = a b → b ∈ V ↔ b ∈ a b
9 7 8 anbi12d ⊢ V = a b → a ∈ V ∧ b ∈ V ↔ a ∈ a b ∧ b ∈ a b
10 6 9 mpbiri ⊢ V = a b → a ∈ V ∧ b ∈ V
11 10 adantl ⊢ a ≠ b ∧ V = a b → a ∈ V ∧ b ∈ V
12 11 pm4.71ri ⊢ a ≠ b ∧ V = a b ↔ a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b
13 12 2exbii ⊢ ∃ a ∃ b a ≠ b ∧ V = a b ↔ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b
14 13 a1i ⊢ V ∈ W → ∃ a ∃ b a ≠ b ∧ V = a b ↔ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b
15 r2ex ⊢ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ V = a b ↔ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b
16 15 bicomi ⊢ ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b ↔ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ V = a b
17 16 a1i ⊢ V ∈ W → ∃ a ∃ b a ∈ V ∧ b ∈ V ∧ a ≠ b ∧ V = a b ↔ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ V = a b
18 1 14 17 3bitrd ⊢ V ∈ W → V = 2 ↔ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ V = a b