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 e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } e. ~P C ) )

Proof

Step Hyp Ref Expression
1 prssg
 |-  ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } C_ C ) )
2 prex
 |-  { A , B } e. _V
3 2 elpw
 |-  ( { A , B } e. ~P C <-> { A , B } C_ C )
4 1 3 bitr4di
 |-  ( ( A e. V /\ B e. W ) -> ( ( A e. C /\ B e. C ) <-> { A , B } e. ~P C ) )