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	|- ( Disj_ x e. B C -> Disj_ x e. B ( C i^i A ) )

Proof

Step	Hyp	Ref	Expression
1		elinel1	|- ( y e. ( C i^i A ) -> y e. C )
2	1	rmoimi	|- ( E* x e. B y e. C -> E* x e. B y e. ( C i^i A ) )
3	2	alimi	|- ( A. y E* x e. B y e. C -> A. y E* x e. B y e. ( C i^i A ) )
4		df-disj	|- ( Disj_ x e. B C <-> A. y E* x e. B y e. C )
5		df-disj	|- ( Disj_ x e. B ( C i^i A ) <-> A. y E* x e. B y e. ( C i^i A ) )
6	3 4 5	3imtr4i	|- ( Disj_ x e. B C -> Disj_ x e. B ( C i^i A ) )