Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Alexander van der Vekens
Unordered pairs
Set of unordered pairs
prssspr
Metamath Proof Explorer
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