Metamath Proof Explorer

Theorem prelpw

Description: A pair of two sets belongs to the power class of a class containing those two sets and vice versa. (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