Metamath Proof Explorer

Theorem ssiun

Description: Subset implication for an indexed union. (Contributed by NM, 3-Sep-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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

Proof

Step Hyp Ref Expression
1 ssel 
 |-  ( C C_ B -> ( y e. C -> y e. B ) )
2 1 reximi 
 |-  ( E. x e. A C C_ B -> E. x e. A ( y e. C -> y e. B ) )
3 r19.37v 
 |-  ( E. x e. A ( y e. C -> y e. B ) -> ( y e. C -> E. x e. A y e. B ) )
4 2 3 syl 
 |-  ( E. x e. A C C_ B -> ( y e. C -> E. x e. A y e. B ) )
5 eliun 
 |-  ( y e. U_ x e. A B <-> E. x e. A y e. B )
6 4 5 syl6ibr 
 |-  ( E. x e. A C C_ B -> ( y e. C -> y e. U_ x e. A B ) )
7 6 ssrdv 
 |-  ( E. x e. A C C_ B -> C C_ U_ x e. A B )