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∈Vp=ab

Proof

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