Metamath Proof Explorer


Theorem prprvalpw

Description: The set of all proper unordered pairs over a given set V , expressed by a restricted class abstraction. (Contributed by AV, 29-Apr-2023)

Ref Expression
Assertion prprvalpw V W PrPairs V = p 𝒫 V | a V b V a b p = a b

Proof

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