This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )