This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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