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 ∈ V p = a b

Proof

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