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∈Va≠b∧p=ab

Proof

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