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 syl6bi 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