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 e. _V
prsspw.2
|- B e. _V
Assertion prsspw
|- ( { A , B } C_ ~P C <-> ( A C_ C /\ B C_ C ) )

Proof

Step Hyp Ref Expression
1 prsspw.1
 |-  A e. _V
2 prsspw.2
 |-  B e. _V
3 prsspwg
 |-  ( ( A e. _V /\ B e. _V ) -> ( { A , B } C_ ~P C <-> ( A C_ C /\ B C_ C ) ) )
4 1 2 3 mp2an
 |-  ( { A , B } C_ ~P C <-> ( A C_ C /\ B C_ C ) )