Metamath Proof Explorer

Theorem sprvalpwle2

Description: The set of all unordered pairs over a given set V , expressed by a restricted class abstraction. (Contributed by AV, 24-Nov-2021)

Ref Expression
Assertion sprvalpwle2 ⊢ V ∈ W → Pairs ⁡ V = p ∈ 𝒫 V ∖ ∅ | p ≤ 2

Proof

Step Hyp Ref Expression
1 sprvalpwn0 ⊢ V ∈ W → Pairs ⁡ V = p ∈ 𝒫 V ∖ ∅ | ∃ a ∈ V ∃ b ∈ V p = a b
2 hashle2prv ⊢ p ∈ 𝒫 V ∖ ∅ → p ≤ 2 ↔ ∃ a ∈ V ∃ b ∈ V p = a b
3 2 adantl ⊢ V ∈ W ∧ p ∈ 𝒫 V ∖ ∅ → p ≤ 2 ↔ ∃ a ∈ V ∃ b ∈ V p = a b
4 3 bicomd ⊢ V ∈ W ∧ p ∈ 𝒫 V ∖ ∅ → ∃ a ∈ V ∃ b ∈ V p = a b ↔ p ≤ 2
5 4 rabbidva ⊢ V ∈ W → p ∈ 𝒫 V ∖ ∅ | ∃ a ∈ V ∃ b ∈ V p = a b = p ∈ 𝒫 V ∖ ∅ | p ≤ 2
6 1 5 eqtrd ⊢ V ∈ W → Pairs ⁡ V = p ∈ 𝒫 V ∖ ∅ | p ≤ 2