Theorem disjss1f

Description: A subset of a disjoint collection is disjoint. (Contributed by Thierry Arnoux, 6-Apr-2017)

	Ref	Expression
Hypotheses	disjss1f.1	$$⊢\underset{\_}{Ⅎ}xA$$
	disjss1f.2	$$⊢\underset{\_}{Ⅎ}xB$$
Assertion	disjss1f	$$⊢A\subseteq B\to \left(\underset{x\in B}{Disj}C\to \underset{x\in A}{Disj}C\right)$$

Proof

Step	Hyp	Ref	Expression
1		disjss1f.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		disjss1f.2	$$⊢\underset{\_}{Ⅎ}xB$$
3	1 2	ssrmof	$$⊢A\subseteq B\to \left({\exists }^{*}x\in By\in C\to {\exists }^{*}x\in Ay\in C\right)$$
4	3	alimdv	$$⊢A\subseteq B\to \left(\forall y{\exists }^{*}x\in By\in C\to \forall y{\exists }^{*}x\in Ay\in C\right)$$
5		df-disj	$$⊢\underset{x\in B}{Disj}C\leftrightarrow \forall y{\exists }^{*}x\in By\in C$$
6		df-disj	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \forall y{\exists }^{*}x\in Ay\in C$$
7	4 5 6	3imtr4g	$$⊢A\subseteq B\to \left(\underset{x\in B}{Disj}C\to \underset{x\in A}{Disj}C\right)$$