Theorem prelpw

Description: A pair of two sets belongs to the power class of a class containing those two sets and vice versa. (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 ) )