funfv

Description: A simplified expression for the value of a function when we know it is a function. (Contributed by NM, 22-May-1998)

		Ref	Expression
	Assertion	funfv	$⊢ Fun F \to F (A) = ⋃ F [\{A\}]$

Step	Hyp	Ref	Expression
1		fvex	$⊢ F (A) \in V$
2	1	unisn	$⊢ ⋃ \{F (A)\} = F (A)$
3		eqid	$⊢ dom F = dom F$
4		df-fn	$⊢ F Fn dom F \leftrightarrow (Fun F \land dom F = dom F)$
5	3 4	mpbiran2	$⊢ F Fn dom F \leftrightarrow Fun F$
6		fnsnfv	$⊢ (F Fn dom F \land A \in dom F) \to \{F (A)\} = F [\{A\}]$
7	5 6	sylanbr	$⊢ (Fun F \land A \in dom F) \to \{F (A)\} = F [\{A\}]$
8	7	unieqd	$⊢ (Fun F \land A \in dom F) \to ⋃ \{F (A)\} = ⋃ F [\{A\}]$
9	2 8	eqtr3id	$⊢ (Fun F \land A \in dom F) \to F (A) = ⋃ F [\{A\}]$
10	9	ex	$⊢ Fun F \to (A \in dom F \to F (A) = ⋃ F [\{A\}])$
11		ndmfv	$⊢ \neg A \in dom F \to F (A) = \emptyset$
12		ndmima	$⊢ \neg A \in dom F \to F [\{A\}] = \emptyset$
13	12	unieqd	$⊢ \neg A \in dom F \to ⋃ F [\{A\}] = ⋃ \emptyset$
14		uni0	$⊢ ⋃ \emptyset = \emptyset$
15	13 14	eqtrdi	$⊢ \neg A \in dom F \to ⋃ F [\{A\}] = \emptyset$
16	11 15	eqtr4d	$⊢ \neg A \in dom F \to F (A) = ⋃ F [\{A\}]$
17	10 16	pm2.61d1	$⊢ Fun F \to F (A) = ⋃ F [\{A\}]$

Metamath Proof Explorer