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

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 ⊢ Fun ⁡ F → F = ⋃ x ∈ dom ⁡ F x F ⁡ x

Proof

Step Hyp Ref Expression
1 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
2 dffn5 ⊢ F Fn dom ⁡ F ↔ F = x ∈ dom ⁡ F ⟼ F ⁡ x
3 1 2 sylbb ⊢ Fun ⁡ F → F = x ∈ dom ⁡ F ⟼ F ⁡ x
4 fvex ⊢ F ⁡ x ∈ V
5 4 dfmpt ⊢ x ∈ dom ⁡ F ⟼ F ⁡ x = ⋃ x ∈ dom ⁡ F x F ⁡ x
6 3 5 eqtrdi ⊢ Fun ⁡ F → F = ⋃ x ∈ dom ⁡ F x F ⁡ x