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 V B W A C B C A B 𝒫 C

Proof

Step Hyp Ref Expression
1 prssg A V B W A C B C A B C
2 prex A B V
3 2 elpw A B 𝒫 C A B C
4 1 3 bitr4di A V B W A C B C A B 𝒫 C