Metamath Proof Explorer

Theorem prelpw

Description: An unordered pair of two sets is a member of the powerclass of a class if and only if the two sets are members of that class. (Contributed by AV, 8-Jan-2020)

Ref Expression
Assertion prelpw ⊢ A ∈ V ∧ B ∈ W → A ∈ C ∧ B ∈ C ↔ A B ∈ 𝒫 C

Proof

Step Hyp Ref Expression
1 prssg ⊢ A ∈ V ∧ B ∈ W → A ∈ C ∧ B ∈ C ↔ A B ⊆ C
2 prex ⊢ A B ∈ V
3 2 elpw ⊢ A B ∈ 𝒫 C ↔ A B ⊆ C
4 1 3 bitr4di ⊢ A ∈ V ∧ B ∈ W → A ∈ C ∧ B ∈ C ↔ A B ∈ 𝒫 C