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 e. V -> ( A i^i ~P B ) = { x e. A | x C_ B } )

Proof

Step Hyp Ref Expression
1 dfin5 
 |-  ( A i^i ~P B ) = { x e. A | x e. ~P B }
2 elpw2g 
 |-  ( B e. V -> ( x e. ~P B <-> x C_ B ) )
3 2 rabbidv 
 |-  ( B e. V -> { x e. A | x e. ~P B } = { x e. A | x C_ B } )
4 1 3 eqtrid 
 |-  ( B e. V -> ( A i^i ~P B ) = { x e. A | x C_ B } )