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 ( ( 𝐴𝐶𝐵𝐶 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝐶 )

Proof

Step Hyp Ref Expression
1 prelpw ( ( 𝐴𝐶𝐵𝐶 ) → ( ( 𝐴𝐶𝐵𝐶 ) ↔ { 𝐴 , 𝐵 } ∈ 𝒫 𝐶 ) )
2 1 ibi ( ( 𝐴𝐶𝐵𝐶 ) → { 𝐴 , 𝐵 } ∈ 𝒫 𝐶 )