Theorem intunsn

Description: Theorem joining a singleton to an intersection. (Contributed by NM, 29-Sep-2002)

	Ref	Expression
Hypothesis	intunsn.1	$$⊢B\in \mathrm{V}$$
Assertion	intunsn	$$⊢\bigcap \left(A\cup \left\{B\right\}\right)=\bigcap A\cap B$$

Proof

Step	Hyp	Ref	Expression
1		intunsn.1	$$⊢B\in \mathrm{V}$$
2		intun	$$⊢\bigcap \left(A\cup \left\{B\right\}\right)=\bigcap A\cap \bigcap \left\{B\right\}$$
3	1	intsn	$$⊢\bigcap \left\{B\right\}=B$$
4	3	ineq2i	$$⊢\bigcap A\cap \bigcap \left\{B\right\}=\bigcap A\cap B$$
5	2 4	eqtri	$$⊢\bigcap \left(A\cup \left\{B\right\}\right)=\bigcap A\cap B$$