inintabss

Description: Upper bound on intersection of class and the intersection of a class. (Contributed by RP, 13-Aug-2020)

		Ref	Expression
	Assertion	inintabss	$⊢ A \cap ⋂ \{x \| φ\} \subseteq ⋂ \{w \in 𝒫 A \| \exists x (w = A \cap x \land φ)\}$

Step	Hyp	Ref	Expression
1		ax-1	$⊢ u \in A \to (\exists x φ \to u \in A)$
2	1	anim1i	$⊢ (u \in A \land \forall x (φ \to u \in x)) \to ((\exists x φ \to u \in A) \land \forall x (φ \to u \in x))$
3		elinintab	$⊢ u \in (A \cap ⋂ \{x \| φ\}) \leftrightarrow (u \in A \land \forall x (φ \to u \in x))$
4		elinintrab	$⊢ u \in V \to (u \in ⋂ \{w \in 𝒫 A \| \exists x (w = A \cap x \land φ)\} \leftrightarrow ((\exists x φ \to u \in A) \land \forall x (φ \to u \in x)))$
5	4	elv	$⊢ u \in ⋂ \{w \in 𝒫 A \| \exists x (w = A \cap x \land φ)\} \leftrightarrow ((\exists x φ \to u \in A) \land \forall x (φ \to u \in x))$
6	2 3 5	3imtr4i	$⊢ u \in (A \cap ⋂ \{x \| φ\}) \to u \in ⋂ \{w \in 𝒫 A \| \exists x (w = A \cap x \land φ)\}$
7	6	ssriv	$⊢ A \cap ⋂ \{x \| φ\} \subseteq ⋂ \{w \in 𝒫 A \| \exists x (w = A \cap x \land φ)\}$

Metamath Proof Explorer