This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem intss

Description: Intersection of subclasses. (Contributed by NM, 14-Oct-1999) (Proof shortened by OpenAI, 25-Mar-2020)

		Ref	Expression
	Assertion	intss	$⊢ A \subseteq B \to ⋂ B \subseteq ⋂ A$

Step	Hyp	Ref	Expression
1		ssralv	$⊢ A \subseteq B \to (\forall x \in B y \in x \to \forall x \in A y \in x)$
2	1	ss2abdv	$⊢ A \subseteq B \to \{y \| \forall x \in B y \in x\} \subseteq \{y \| \forall x \in A y \in x\}$
3		dfint2	$⊢ ⋂ B = \{y \| \forall x \in B y \in x\}$
4		dfint2	$⊢ ⋂ A = \{y \| \forall x \in A y \in x\}$
5	2 3 4	3sstr4g	$⊢ A \subseteq B \to ⋂ B \subseteq ⋂ A$