Metamath Proof Explorer

Theorem ssiun2s

Description: Subset relationship for an indexed union. (Contributed by NM, 26-Oct-2003)

Ref Expression
Hypothesis ssiun2s.1 
|- ( x = C -> B = D )
Assertion ssiun2s 
|- ( C e. A -> D C_ U_ x e. A B )

Proof

Step Hyp Ref Expression
1 ssiun2s.1 
 |-  ( x = C -> B = D )
2 nfcv 
 |-  F/_ x C
3 nfcv 
 |-  F/_ x D
4 nfiu1 
 |-  F/_ x U_ x e. A B
5 3 4 nfss 
 |-  F/ x D C_ U_ x e. A B
6 1 sseq1d 
 |-  ( x = C -> ( B C_ U_ x e. A B <-> D C_ U_ x e. A B ) )
7 ssiun2 
 |-  ( x e. A -> B C_ U_ x e. A B )
8 2 5 6 7 vtoclgaf 
 |-  ( C e. A -> D C_ U_ x e. A B )