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	⊢ 𝒫 ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝒫 𝑥

Proof

Step	Hyp	Ref	Expression
1		ssint	⊢ ( 𝑦 ⊆ ∩ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥 )
2		velpw	⊢ ( 𝑦 ∈ 𝒫 𝑥 ↔ 𝑦 ⊆ 𝑥 )
3	2	ralbii	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝒫 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ⊆ 𝑥 )
4	1 3	bitr4i	⊢ ( 𝑦 ⊆ ∩ 𝐴 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝒫 𝑥 )
5		velpw	⊢ ( 𝑦 ∈ 𝒫 ∩ 𝐴 ↔ 𝑦 ⊆ ∩ 𝐴 )
6		eliin	⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝒫 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝒫 𝑥 ) )
7	6	elv	⊢ ( 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝒫 𝑥 ↔ ∀ 𝑥 ∈ 𝐴 𝑦 ∈ 𝒫 𝑥 )
8	4 5 7	3bitr4i	⊢ ( 𝑦 ∈ 𝒫 ∩ 𝐴 ↔ 𝑦 ∈ ∩ 𝑥 ∈ 𝐴 𝒫 𝑥 )
9	8	eqriv	⊢ 𝒫 ∩ 𝐴 = ∩ 𝑥 ∈ 𝐴 𝒫 𝑥