Metamath Proof Explorer

Theorem prsspwg

Description: An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by Thierry Arnoux, 3-Oct-2016) (Revised by NM, 18-Jan-2018)

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

Proof

Step Hyp Ref Expression
1 prssg ⊢ A ∈ V ∧ B ∈ W → A ∈ 𝒫 C ∧ B ∈ 𝒫 C ↔ A B ⊆ 𝒫 C
2 elpwg ⊢ A ∈ V → A ∈ 𝒫 C ↔ A ⊆ C
3 elpwg ⊢ B ∈ W → B ∈ 𝒫 C ↔ B ⊆ C
4 2 3 bi2anan9 ⊢ A ∈ V ∧ B ∈ W → A ∈ 𝒫 C ∧ B ∈ 𝒫 C ↔ A ⊆ C ∧ B ⊆ C
5 1 4 bitr3d ⊢ A ∈ V ∧ B ∈ W → A B ⊆ 𝒫 C ↔ A ⊆ C ∧ B ⊆ C