Metamath Proof Explorer

Theorem prssspr

Description: An element of a subset 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 prssspr ⊢ P ⊆ Pairs ⁡ V ∧ X ∈ P → ∃ a ∈ V ∃ b ∈ V X = a b

Proof

Step Hyp Ref Expression
1 ssel2 ⊢ P ⊆ Pairs ⁡ V ∧ X ∈ P → X ∈ Pairs ⁡ V
2 sprel ⊢ X ∈ Pairs ⁡ V → ∃ a ∈ V ∃ b ∈ V X = a b
3 1 2 syl ⊢ P ⊆ Pairs ⁡ V ∧ X ∈ P → ∃ a ∈ V ∃ b ∈ V X = a b