Metamath Proof Explorer

Theorem sprel

Description: An element of the set of all unordered pairs over a given set V is a pair of elements of the set V . (Contributed by AV, 22-Nov-2021)

Ref Expression
Assertion sprel ⊢ X ∈ Pairs ⁡ V → ∃ a ∈ V ∃ b ∈ V X = a b

Proof

Step Hyp Ref Expression
1 elfvex ⊢ X ∈ Pairs ⁡ V → V ∈ V
2 sprvalpw ⊢ V ∈ V → Pairs ⁡ V = p ∈ 𝒫 V | ∃ a ∈ V ∃ b ∈ V p = a b
3 2 eleq2d ⊢ V ∈ V → X ∈ Pairs ⁡ V ↔ X ∈ p ∈ 𝒫 V | ∃ a ∈ V ∃ b ∈ V p = a b
4 eqeq1 ⊢ p = X → p = a b ↔ X = a b
5 4 2rexbidv ⊢ p = X → ∃ a ∈ V ∃ b ∈ V p = a b ↔ ∃ a ∈ V ∃ b ∈ V X = a b
6 5 elrab ⊢ X ∈ p ∈ 𝒫 V | ∃ a ∈ V ∃ b ∈ V p = a b ↔ X ∈ 𝒫 V ∧ ∃ a ∈ V ∃ b ∈ V X = a b
7 6 simprbi ⊢ X ∈ p ∈ 𝒫 V | ∃ a ∈ V ∃ b ∈ V p = a b → ∃ a ∈ V ∃ b ∈ V X = a b
8 3 7 biimtrdi ⊢ V ∈ V → X ∈ Pairs ⁡ V → ∃ a ∈ V ∃ b ∈ V X = a b
9 1 8 mpcom ⊢ X ∈ Pairs ⁡ V → ∃ a ∈ V ∃ b ∈ V X = a b