iinss1

Description: Subclass theorem for indexed intersection. (Contributed by NM, 24-Jan-2012)

		Ref	Expression
	Assertion	iinss1	$⊢ A \subseteq B \to ⋂_{x \in B} C \subseteq ⋂_{x \in A} C$

Step	Hyp	Ref	Expression
1		ssralv	$⊢ A \subseteq B \to (\forall x \in B y \in C \to \forall x \in A y \in C)$
2		eliin	$⊢ y \in V \to (y \in ⋂_{x \in B} C \leftrightarrow \forall x \in B y \in C)$
3	2	elv	$⊢ y \in ⋂_{x \in B} C \leftrightarrow \forall x \in B y \in C$
4		eliin	$⊢ y \in V \to (y \in ⋂_{x \in A} C \leftrightarrow \forall x \in A y \in C)$
5	4	elv	$⊢ y \in ⋂_{x \in A} C \leftrightarrow \forall x \in A y \in C$
6	1 3 5	3imtr4g	$⊢ A \subseteq B \to (y \in ⋂_{x \in B} C \to y \in ⋂_{x \in A} C)$
7	6	ssrdv	$⊢ A \subseteq B \to ⋂_{x \in B} C \subseteq ⋂_{x \in A} C$

Metamath Proof Explorer