Metamath Proof Explorer


Theorem iinpw

Description: The power class of an intersection in terms of indexed intersection. Exercise 24(a) of Enderton p. 33. (Contributed by NM, 29-Nov-2003)

Ref Expression
Assertion iinpw 𝒫A=xA𝒫x

Proof

Step Hyp Ref Expression
1 ssint yAxAyx
2 velpw y𝒫xyx
3 2 ralbii xAy𝒫xxAyx
4 1 3 bitr4i yAxAy𝒫x
5 velpw y𝒫AyA
6 eliin yVyxA𝒫xxAy𝒫x
7 6 elv yxA𝒫xxAy𝒫x
8 4 5 7 3bitr4i y𝒫AyxA𝒫x
9 8 eqriv 𝒫A=xA𝒫x