Theorem disjin

Description: If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 14-Feb-2017)

	Ref	Expression
Assertion	disjin	$$⊢\underset{x\in B}{Disj}C\to \underset{x\in B}{Disj}\left(C\cap A\right)$$

Proof

Step	Hyp	Ref	Expression
1		elinel1	$$⊢y\in \left(C\cap A\right)\to y\in C$$
2	1	rmoimi	$$⊢{\exists }^{*}x\in By\in C\to {\exists }^{*}x\in By\in \left(C\cap A\right)$$
3	2	alimi	$$⊢\forall y{\exists }^{*}x\in By\in C\to \forall y{\exists }^{*}x\in By\in \left(C\cap A\right)$$
4		df-disj	$$⊢\underset{x\in B}{Disj}C\leftrightarrow \forall y{\exists }^{*}x\in By\in C$$
5		df-disj	$$⊢\underset{x\in B}{Disj}\left(C\cap A\right)\leftrightarrow \forall y{\exists }^{*}x\in By\in \left(C\cap A\right)$$
6	3 4 5	3imtr4i	$$⊢\underset{x\in B}{Disj}C\to \underset{x\in B}{Disj}\left(C\cap A\right)$$