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 \to F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\}$

Step	Hyp	Ref	Expression
1		funfn	$⊢ Fun F \leftrightarrow F Fn dom F$
2		dffn5	$⊢ F Fn dom F \leftrightarrow F = (x \in dom F ⟼ F (x))$
3	1 2	sylbb	$⊢ Fun F \to F = (x \in dom F ⟼ F (x))$
4		fvex	$⊢ F (x) \in V$
5	4	dfmpt	$⊢ (x \in dom F ⟼ F (x)) = ⋃_{x \in dom F} \{⟨x, F (x)⟩\}$
6	3 5	eqtrdi	$⊢ Fun F \to F = ⋃_{x \in dom F} \{⟨x, F (x)⟩\}$