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

Proof

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