Metamath Proof Explorer


Theorem funiun

Description: A function is a union of singletons of ordered pairs indexed by its domain. (Contributed by AV, 18-Sep-2020)

Ref Expression
Assertion funiun FunFF=xdomFxFx

Proof

Step Hyp Ref Expression
1 funfn FunFFFndomF
2 dffn5 FFndomFF=xdomFFx
3 1 2 sylbb FunFF=xdomFFx
4 fvex FxV
5 4 dfmpt xdomFFx=xdomFxFx
6 3 5 eqtrdi FunFF=xdomFxFx