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