Metamath Proof Explorer

Theorem ss2iun

Description: Subclass theorem for indexed union. (Contributed by NM, 26-Nov-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion ss2iun 
|- ( A. x e. A B C_ C -> U_ x e. A B C_ U_ x e. A C )

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 rexim 
 |-  ( A. x e. A ( y e. B -> y e. C ) -> ( E. x e. A y e. B -> E. x e. A y e. C ) )
4 2 3 syl 
 |-  ( A. x e. A B C_ C -> ( E. x e. A y e. B -> E. x e. A y e. C ) )
5 eliun 
 |-  ( y e. U_ x e. A B <-> E. x e. A y e. B )
6 eliun 
 |-  ( y e. U_ x e. A C <-> E. x e. A y e. C )
7 4 5 6 3imtr4g 
 |-  ( A. x e. A B C_ C -> ( y e. U_ x e. A B -> y e. U_ x e. A C ) )
8 7 ssrdv 
 |-  ( A. x e. A B C_ C -> U_ x e. A B C_ U_ x e. A C )