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