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	$$⊢\phi \to A\in 𝒫C$$
Assertion	elpwincl1	$$⊢\phi \to A\cap B\in 𝒫C$$

Proof

Step	Hyp	Ref	Expression
1		elpwincl.1	$$⊢\phi \to A\in 𝒫C$$
2		elpwi	$$⊢A\in 𝒫C\to A\subseteq C$$
3		ssinss1	$$⊢A\subseteq C\to A\cap B\subseteq C$$
4	1 2 3	3syl	$$⊢\phi \to A\cap B\subseteq C$$
5		inex1g	$$⊢A\in 𝒫C\to A\cap B\in \mathrm{V}$$
6		elpwg	$$⊢A\cap B\in \mathrm{V}\to \left(A\cap B\in 𝒫C\leftrightarrow A\cap B\subseteq C\right)$$
7	1 5 6	3syl	$$⊢\phi \to \left(A\cap B\in 𝒫C\leftrightarrow A\cap B\subseteq C\right)$$
8	4 7	mpbird	$$⊢\phi \to A\cap B\in 𝒫C$$