Theorem elimaint

Description: Element of image of intersection. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	elimaint	$$⊢y\in \bigcap A\left[B\right]\leftrightarrow \exists b\in B\forall a\in A⟨b,y⟩\in a$$

Proof

Step	Hyp	Ref	Expression
1		vex	$$⊢y\in \mathrm{V}$$
2	1	elima	$$⊢y\in \bigcap A\left[B\right]\leftrightarrow \exists b\in Bb\bigcap Ay$$
3		df-br	$$⊢b\bigcap Ay\leftrightarrow ⟨b,y⟩\in \bigcap A$$
4		opex	$$⊢⟨b,y⟩\in \mathrm{V}$$
5	4	elint2	$$⊢⟨b,y⟩\in \bigcap A\leftrightarrow \forall a\in A⟨b,y⟩\in a$$
6	3 5	bitri	$$⊢b\bigcap Ay\leftrightarrow \forall a\in A⟨b,y⟩\in a$$
7	6	rexbii	$$⊢\exists b\in Bb\bigcap Ay\leftrightarrow \exists b\in B\forall a\in A⟨b,y⟩\in a$$
8	2 7	bitri	$$⊢y\in \bigcap A\left[B\right]\leftrightarrow \exists b\in B\forall a\in A⟨b,y⟩\in a$$