Theorem disjin2

Description: If a collection is disjoint, so is the collection of the intersections with a given set. (Contributed by Thierry Arnoux, 21-Jun-2020)

	Ref	Expression
Assertion	disjin2	|- ( Disj_ x e. B C -> Disj_ x e. B ( A i^i C ) )

Proof

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