Metamath Proof Explorer


Theorem inpw

Description: Two ways of expressing a collection of subsets as seen in df-ntr , unimax , and others (Contributed by Zhi Wang, 27-Sep-2024)

Ref Expression
Assertion inpw B V A 𝒫 B = x A | x B

Proof

Step Hyp Ref Expression
1 dfin5 A 𝒫 B = x A | x 𝒫 B
2 elpw2g B V x 𝒫 B x B
3 2 rabbidv B V x A | x 𝒫 B = x A | x B
4 1 3 eqtrid B V A 𝒫 B = x A | x B