dmiin

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

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

Metamath Proof Explorer