Theorem dmiin

Description: Domain of an intersection. (Contributed by FL, 15-Oct-2012)

	Ref	Expression
Assertion	dmiin	$$⊢\mathrm{dom}\bigcap _{x\in A}B\subseteq \bigcap _{x\in A}\mathrm{dom}B$$

Proof

Step	Hyp	Ref	Expression
1		nfii1	$$⊢\underset{\_}{Ⅎ}x\bigcap _{x\in A}B$$
2	1	nfdm	$$⊢\underset{\_}{Ⅎ}x\mathrm{dom}\bigcap _{x\in A}B$$
3	2	ssiinf	$$⊢\mathrm{dom}\bigcap _{x\in A}B\subseteq \bigcap _{x\in A}\mathrm{dom}B\leftrightarrow \forall x\in A\mathrm{dom}\bigcap _{x\in A}B\subseteq \mathrm{dom}B$$
4		iinss2	$$⊢x\in A\to \bigcap _{x\in A}B\subseteq B$$
5		dmss	$$⊢\bigcap _{x\in A}B\subseteq B\to \mathrm{dom}\bigcap _{x\in A}B\subseteq \mathrm{dom}B$$
6	4 5	syl	$$⊢x\in A\to \mathrm{dom}\bigcap _{x\in A}B\subseteq \mathrm{dom}B$$
7	3 6	mprgbir	$$⊢\mathrm{dom}\bigcap _{x\in A}B\subseteq \bigcap _{x\in A}\mathrm{dom}B$$