Metamath Proof Explorer


Theorem prelpwi

Description: If two sets are members of a class, then the unordered pair of those two sets is a member of the powerclass of that class. (Contributed by Thierry Arnoux, 10-Mar-2017) (Proof shortened by AV, 23-Oct-2021)

Ref Expression
Assertion prelpwi A C B C A B 𝒫 C

Proof

Step Hyp Ref Expression
1 prelpw A C B C A C B C A B 𝒫 C
2 1 ibi A C B C A B 𝒫 C