Theorem intimasn

Description: Two ways to express the image of a singleton when the relation is an intersection. (Contributed by RP, 13-Apr-2020)

	Ref	Expression
Assertion	intimasn	$$⊢B\in V\to \bigcap A\left[\left\{B\right\}\right]=\bigcap \left\{x|\exists a\in Ax=a\left[\left\{B\right\}\right]\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ax-5	$$⊢B\in V\to \forall yB\in V$$
2		r19.12sn	$$⊢B\in V\to \left(\exists b\in \left\{B\right\}\forall a\in A⟨b,y⟩\in a\leftrightarrow \forall a\in A\exists b\in \left\{B\right\}⟨b,y⟩\in a\right)$$
3	2	biimprd	$$⊢B\in V\to \left(\forall a\in A\exists b\in \left\{B\right\}⟨b,y⟩\in a\to \exists b\in \left\{B\right\}\forall a\in A⟨b,y⟩\in a\right)$$
4	3	alimi	$$⊢\forall yB\in V\to \forall y\left(\forall a\in A\exists b\in \left\{B\right\}⟨b,y⟩\in a\to \exists b\in \left\{B\right\}\forall a\in A⟨b,y⟩\in a\right)$$
5		intimag	$$⊢\forall y\left(\forall a\in A\exists b\in \left\{B\right\}⟨b,y⟩\in a\to \exists b\in \left\{B\right\}\forall a\in A⟨b,y⟩\in a\right)\to \bigcap A\left[\left\{B\right\}\right]=\bigcap \left\{x|\exists a\in Ax=a\left[\left\{B\right\}\right]\right\}$$
6	1 4 5	3syl	$$⊢B\in V\to \bigcap A\left[\left\{B\right\}\right]=\bigcap \left\{x|\exists a\in Ax=a\left[\left\{B\right\}\right]\right\}$$