Metamath Proof Explorer

Theorem pwpr

Description: The power set of an unordered pair. (Contributed by NM, 1-May-2009)

Ref Expression
Assertion pwpr ⊢ 𝒫 A B = ∅ A ∪ B A B

Proof

Step Hyp Ref Expression
1 sspr ⊢ x ⊆ A B ↔ x = ∅ ∨ x = A ∨ x = B ∨ x = A B
2 vex ⊢ x ∈ V
3 2 elpr ⊢ x ∈ ∅ A ↔ x = ∅ ∨ x = A
4 2 elpr ⊢ x ∈ B A B ↔ x = B ∨ x = A B
5 3 4 orbi12i ⊢ x ∈ ∅ A ∨ x ∈ B A B ↔ x = ∅ ∨ x = A ∨ x = B ∨ x = A B
6 1 5 bitr4i ⊢ x ⊆ A B ↔ x ∈ ∅ A ∨ x ∈ B A B
7 velpw ⊢ x ∈ 𝒫 A B ↔ x ⊆ A B
8 elun ⊢ x ∈ ∅ A ∪ B A B ↔ x ∈ ∅ A ∨ x ∈ B A B
9 6 7 8 3bitr4i ⊢ x ∈ 𝒫 A B ↔ x ∈ ∅ A ∪ B A B
10 9 eqriv ⊢ 𝒫 A B = ∅ A ∪ B A B