Metamath Proof Explorer


Theorem fviunfun

Description: The function value of an indexed union is the value of one of the indexed functions. (Contributed by AV, 4-Nov-2023)

Ref Expression
Hypothesis fviunfun.u U = i I F i
Assertion fviunfun Fun U J I X dom F J U X = F J X

Proof

Step Hyp Ref Expression
1 fviunfun.u U = i I F i
2 fveq2 i = J F i = F J
3 2 ssiun2s J I F J i I F i
4 3 1 sseqtrrdi J I F J U
5 funssfv Fun U F J U X dom F J U X = F J X
6 4 5 syl3an2 Fun U J I X dom F J U X = F J X