Metamath Proof Explorer


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 ) )