Metamath Proof Explorer

Theorem prsspw

Description: An unordered pair belongs to the power class of a class iff each member belongs to the class. (Contributed by NM, 10-Dec-2003) (Proof shortened by Andrew Salmon, 26-Jun-2011) (Proof shortened by OpenAI, 25-Mar-2020)

Ref Expression
Hypotheses prsspw.1 ⊢ A ∈ V
prsspw.2 ⊢ B ∈ V
Assertion prsspw ⊢ A B ⊆ 𝒫 C ↔ A ⊆ C ∧ B ⊆ C

Proof

Step Hyp Ref Expression
1 prsspw.1 ⊢ A ∈ V
2 prsspw.2 ⊢ B ∈ V
3 prsspwg ⊢ A ∈ V ∧ B ∈ V → A B ⊆ 𝒫 C ↔ A ⊆ C ∧ B ⊆ C
4 1 2 3 mp2an ⊢ A B ⊆ 𝒫 C ↔ A ⊆ C ∧ B ⊆ C