Metamath Proof Explorer


Theorem ssiun2sf

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

Ref Expression
Hypotheses ssiun2sf.1 _xA
ssiun2sf.2 _xC
ssiun2sf.3 _xD
ssiun2sf.4 x=CB=D
Assertion ssiun2sf CADxAB

Proof

Step Hyp Ref Expression
1 ssiun2sf.1 _xA
2 ssiun2sf.2 _xC
3 ssiun2sf.3 _xD
4 ssiun2sf.4 x=CB=D
5 2 1 nfel xCA
6 nfiu1 _xxAB
7 3 6 nfss xDxAB
8 5 7 nfim xCADxAB
9 eleq1 x=CxACA
10 4 sseq1d x=CBxABDxAB
11 9 10 imbi12d x=CxABxABCADxAB
12 ssiun2 xABxAB
13 2 8 11 12 vtoclgf CACADxAB
14 13 pm2.43i CADxAB