disjss1

Description: A subset of a disjoint collection is disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

		Ref	Expression
	Assertion	disjss1	$⊢ A \subseteq B \to (\underset{x \in B}{Disj} C \to \underset{x \in A}{Disj} C)$

Step	Hyp	Ref	Expression
1		ssel	$⊢ A \subseteq B \to (x \in A \to x \in B)$
2	1	anim1d	$⊢ A \subseteq B \to ((x \in A \land y \in C) \to (x \in B \land y \in C))$
3	2	moimdv	$⊢ A \subseteq B \to (\exists^{} x (x \in B \land y \in C) \to \exists^{} x (x \in A \land y \in C))$
4	3	alimdv	$⊢ A \subseteq B \to (\forall y \exists^{} x (x \in B \land y \in C) \to \forall y \exists^{} x (x \in A \land y \in C))$
5		dfdisj2	$⊢ \underset{x \in B}{Disj} C \leftrightarrow \forall y \exists^{*} x (x \in B \land y \in C)$
6		dfdisj2	$⊢ \underset{x \in A}{Disj} C \leftrightarrow \forall y \exists^{*} x (x \in A \land y \in C)$
7	4 5 6	3imtr4g	$⊢ A \subseteq B \to (\underset{x \in B}{Disj} C \to \underset{x \in A}{Disj} C)$

Metamath Proof Explorer