This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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

Step	Hyp	Ref	Expression
1		elpwincl.1	$⊢ φ \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	$⊢ φ \to A \cap B \subseteq C$
5		inex1g	$⊢ A \in 𝒫 C \to A \cap B \in V$
6		elpwg	$⊢ A \cap B \in V \to (A \cap B \in 𝒫 C \leftrightarrow A \cap B \subseteq C)$
7	1 5 6	3syl	$⊢ φ \to (A \cap B \in 𝒫 C \leftrightarrow A \cap B \subseteq C)$
8	4 7	mpbird	$⊢ φ \to A \cap B \in 𝒫 C$