Metamath Proof Explorer


Theorem fniunfv

Description: The indexed union of a function's values is the union of its range. Compare Definition 5.4 of Monk1 p. 50. (Contributed by NM, 27-Sep-2004)

Ref Expression
Assertion fniunfv FFnAxAFx=ranF

Proof

Step Hyp Ref Expression
1 fvex FxV
2 1 dfiun2 xAFx=y|xAy=Fx
3 fnrnfv FFnAranF=y|xAy=Fx
4 3 unieqd FFnAranF=y|xAy=Fx
5 2 4 eqtr4id FFnAxAFx=ranF