Metamath Proof Explorer


Theorem ssiun2sf

Description: Subset relationship for an indexed union. (Contributed by Thierry Arnoux, 31-Dec-2016)

Ref Expression
Hypotheses ssiun2sf.1
|- F/_ x A
ssiun2sf.2
|- F/_ x C
ssiun2sf.3
|- F/_ x D
ssiun2sf.4
|- ( x = C -> B = D )
Assertion ssiun2sf
|- ( C e. A -> D C_ U_ x e. A B )

Proof

Step Hyp Ref Expression
1 ssiun2sf.1
 |-  F/_ x A
2 ssiun2sf.2
 |-  F/_ x C
3 ssiun2sf.3
 |-  F/_ x D
4 ssiun2sf.4
 |-  ( x = C -> B = D )
5 2 1 nfel
 |-  F/ x C e. A
6 nfiu1
 |-  F/_ x U_ x e. A B
7 3 6 nfss
 |-  F/ x D C_ U_ x e. A B
8 5 7 nfim
 |-  F/ x ( C e. A -> D C_ U_ x e. A B )
9 eleq1
 |-  ( x = C -> ( x e. A <-> C e. A ) )
10 4 sseq1d
 |-  ( x = C -> ( B C_ U_ x e. A B <-> D C_ U_ x e. A B ) )
11 9 10 imbi12d
 |-  ( x = C -> ( ( x e. A -> B C_ U_ x e. A B ) <-> ( C e. A -> D C_ U_ x e. A B ) ) )
12 ssiun2
 |-  ( x e. A -> B C_ U_ x e. A B )
13 2 8 11 12 vtoclgf
 |-  ( C e. A -> ( C e. A -> D C_ U_ x e. A B ) )
14 13 pm2.43i
 |-  ( C e. A -> D C_ U_ x e. A B )