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 \bigcap B\subseteq \bigcap A$$

Proof

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