Metamath Proof Explorer


Theorem sprvalpwn0

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 sprvalpwn0 V W Pairs V = p 𝒫 V | a V b V p = a b

Proof

Step Hyp Ref Expression
1 sprvalpw V W Pairs V = p 𝒫 V | a V b V p = a b
2 id p = a b p = a b
3 vex a V
4 3 prnz a b
5 4 a1i p = a b a b
6 2 5 eqnetrd p = a b p
7 6 a1i a V b V p = a b p
8 7 rexlimivv a V b V p = a b p
9 8 adantl p 𝒫 V a V b V p = a b p
10 9 pm4.71ri p 𝒫 V a V b V p = a b p p 𝒫 V a V b V p = a b
11 ancom p p 𝒫 V p 𝒫 V p
12 11 anbi1i p p 𝒫 V a V b V p = a b p 𝒫 V p a V b V p = a b
13 anass p p 𝒫 V a V b V p = a b p p 𝒫 V a V b V p = a b
14 eldifsn p 𝒫 V p 𝒫 V p
15 14 bicomi p 𝒫 V p p 𝒫 V
16 15 anbi1i p 𝒫 V p a V b V p = a b p 𝒫 V a V b V p = a b
17 12 13 16 3bitr3i p p 𝒫 V a V b V p = a b p 𝒫 V a V b V p = a b
18 10 17 bitri p 𝒫 V a V b V p = a b p 𝒫 V a V b V p = a b
19 18 rabbia2 p 𝒫 V | a V b V p = a b = p 𝒫 V | a V b V p = a b
20 1 19 eqtrdi V W Pairs V = p 𝒫 V | a V b V p = a b