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

Proof

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