Metamath Proof Explorer


Theorem sprvalpw

Description: The set of all unordered pairs over a given set V , expressed by a restricted class abstraction. (Contributed by AV, 21-Nov-2021)

Ref Expression
Assertion sprvalpw V W Pairs V = p 𝒫 V | a V b V p = a b

Proof

Step Hyp Ref Expression
1 sprval V W Pairs V = p | a V b V p = a b
2 prssi a V b V a b V
3 eleq1 p = a b p 𝒫 V a b 𝒫 V
4 prex a b V
5 4 elpw a b 𝒫 V a b V
6 3 5 bitrdi p = a b p 𝒫 V a b V
7 2 6 syl5ibrcom a V b V p = a b p 𝒫 V
8 7 rexlimivv a V b V p = a b p 𝒫 V
9 8 pm4.71ri a V b V p = a b p 𝒫 V a V b V p = a b
10 9 a1i V W a V b V p = a b p 𝒫 V a V b V p = a b
11 10 abbidv V W p | a V b V p = a b = p | p 𝒫 V a V b V p = a b
12 df-rab p 𝒫 V | a V b V p = a b = p | p 𝒫 V a V b V p = a b
13 11 12 eqtr4di V W p | a V b V p = a b = p 𝒫 V | a V b V p = a b
14 1 13 eqtrd V W Pairs V = p 𝒫 V | a V b V p = a b