Metamath Proof Explorer

Theorem iunss1

Description: Subclass theorem for indexed union. (Contributed by NM, 10-Dec-2004) (Proof shortened by Andrew Salmon, 25-Jul-2011)

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

Proof

Step Hyp Ref Expression
1 ssrexv 
 |-  ( A C_ B -> ( E. x e. A y e. C -> E. x e. B y e. C ) )
2 eliun 
 |-  ( y e. U_ x e. A C <-> E. x e. A y e. C )
3 eliun 
 |-  ( y e. U_ x e. B C <-> E. x e. B y e. C )
4 1 2 3 3imtr4g 
 |-  ( A C_ B -> ( y e. U_ x e. A C -> y e. U_ x e. B C ) )
5 4 ssrdv 
 |-  ( A C_ B -> U_ x e. A C C_ U_ x e. B C )