Theorem elpwincl1

Description: Closure of intersection with regard to elementhood to a power set. (Contributed by Thierry Arnoux, 18-May-2020)

	Ref	Expression
Hypothesis	elpwincl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝐶 )
Assertion	elpwincl1	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ 𝒫 𝐶 )

Proof

Step	Hyp	Ref	Expression
1		elpwincl.1	⊢ ( 𝜑 → 𝐴 ∈ 𝒫 𝐶 )
2		elpwi	⊢ ( 𝐴 ∈ 𝒫 𝐶 → 𝐴 ⊆ 𝐶 )
3		ssinss1	⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 )
4	1 2 3	3syl	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 )
5		inex1g	⊢ ( 𝐴 ∈ 𝒫 𝐶 → ( 𝐴 ∩ 𝐵 ) ∈ V )
6		elpwg	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ V → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝒫 𝐶 ↔ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ) )
7	1 5 6	3syl	⊢ ( 𝜑 → ( ( 𝐴 ∩ 𝐵 ) ∈ 𝒫 𝐶 ↔ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐶 ) )
8	4 7	mpbird	⊢ ( 𝜑 → ( 𝐴 ∩ 𝐵 ) ∈ 𝒫 𝐶 )