Metamath Proof Explorer


Theorem prelpwi

Description: A pair of two sets belongs to the power class of a class containing those two sets. (Contributed by Thierry Arnoux, 10-Mar-2017) (Proof shortened by AV, 23-Oct-2021)

Ref Expression
Assertion prelpwi
|- ( ( A e. C /\ B e. C ) -> { A , B } e. ~P C )

Proof

Step Hyp Ref Expression
1 prelpw
 |-  ( ( A e. C /\ B e. C ) -> ( ( A e. C /\ B e. C ) <-> { A , B } e. ~P C ) )
2 1 ibi
 |-  ( ( A e. C /\ B e. C ) -> { A , B } e. ~P C )