Theorem disjss2

Description: If each element of a collection is contained in a disjoint collection, the original collection is also disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Assertion	disjss2	|- ( A. x e. A B C_ C -> ( Disj_ x e. A C -> Disj_ x e. A B ) )

Proof

Step	Hyp	Ref	Expression
1		ssel	|- ( B C_ C -> ( y e. B -> y e. C ) )
2	1	ralimi	|- ( A. x e. A B C_ C -> A. x e. A ( y e. B -> y e. C ) )
3		rmoim	|- ( A. x e. A ( y e. B -> y e. C ) -> ( E* x e. A y e. C -> E* x e. A y e. B ) )
4	2 3	syl	|- ( A. x e. A B C_ C -> ( E* x e. A y e. C -> E* x e. A y e. B ) )
5	4	alimdv	|- ( A. x e. A B C_ C -> ( A. y E* x e. A y e. C -> A. y E* x e. A y e. B ) )
6		df-disj	|- ( Disj_ x e. A C <-> A. y E* x e. A y e. C )
7		df-disj	|- ( Disj_ x e. A B <-> A. y E* x e. A y e. B )
8	5 6 7	3imtr4g	|- ( A. x e. A B C_ C -> ( Disj_ x e. A C -> Disj_ x e. A B ) )