inintabd

Description: Value of the intersection of class with the intersection of a nonempty class. (Contributed by RP, 13-Aug-2020)

		Ref	Expression
	Hypothesis	inintabd.x	$⊢ φ \to \exists x ψ$
	Assertion	inintabd	$⊢ φ \to A \cap ⋂ \{x \| ψ\} = ⋂ \{w \in 𝒫 A \| \exists x (w = A \cap x \land ψ)\}$

Step	Hyp	Ref	Expression
1		inintabd.x	$⊢ φ \to \exists x ψ$
2		pm5.5	$⊢ \exists x ψ \to ((\exists x ψ \to u \in A) \leftrightarrow u \in A)$
3	1 2	syl	$⊢ φ \to ((\exists x ψ \to u \in A) \leftrightarrow u \in A)$
4	3	bicomd	$⊢ φ \to (u \in A \leftrightarrow (\exists x ψ \to u \in A))$
5	4	anbi1d	$⊢ φ \to ((u \in A \land \forall x (ψ \to u \in x)) \leftrightarrow ((\exists x ψ \to u \in A) \land \forall x (ψ \to u \in x)))$
6		elinintab	$⊢ u \in (A \cap ⋂ \{x \| ψ\}) \leftrightarrow (u \in A \land \forall x (ψ \to u \in x))$
7		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)))$
8	7	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))$
9	5 6 8	3bitr4g	$⊢ φ \to (u \in (A \cap ⋂ \{x \| ψ\}) \leftrightarrow u \in ⋂ \{w \in 𝒫 A \| \exists x (w = A \cap x \land ψ)\})$
10	9	eqrdv	$⊢ φ \to A \cap ⋂ \{x \| ψ\} = ⋂ \{w \in 𝒫 A \| \exists x (w = A \cap x \land ψ)\}$

Metamath Proof Explorer