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

Metamath Proof Explorer

Theorem hash2sspr

Description: A subset of size two is an unordered pair of elements of its superset. (Contributed by Alexander van der Vekens, 12-Jul-2017) (Proof shortened by AV, 4-Nov-2020)

Ref Expression
Assertion hash2sspr ⊢ P ∈ 𝒫 V ∧ P = 2 → ∃ a ∈ V ∃ b ∈ V P = a b

Proof

Step Hyp Ref Expression
1 fveqeq2 ⊢ p = P → p = 2 ↔ P = 2
2 1 elrab ⊢ P ∈ p ∈ 𝒫 V | p = 2 ↔ P ∈ 𝒫 V ∧ P = 2
3 elss2prb ⊢ P ∈ p ∈ 𝒫 V | p = 2 ↔ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ P = a b
4 simpr ⊢ a ≠ b ∧ P = a b → P = a b
5 4 reximi ⊢ ∃ b ∈ V a ≠ b ∧ P = a b → ∃ b ∈ V P = a b
6 5 reximi ⊢ ∃ a ∈ V ∃ b ∈ V a ≠ b ∧ P = a b → ∃ a ∈ V ∃ b ∈ V P = a b
7 3 6 sylbi ⊢ P ∈ p ∈ 𝒫 V | p = 2 → ∃ a ∈ V ∃ b ∈ V P = a b
8 2 7 sylbir ⊢ P ∈ 𝒫 V ∧ P = 2 → ∃ a ∈ V ∃ b ∈ V P = a b