Metamath Proof Explorer

Theorem fundmdfat

Description: A function is defined at any element of its domain. (Contributed by AV, 2-Sep-2022)

		Ref	Expression
	Assertion	fundmdfat	$⊢ (Fun F \land A \in dom F) \to F defAt A$

Step	Hyp	Ref	Expression
1		funres	$⊢ Fun F \to Fun ({F ↾}_{\{A\}})$
2	1	anim1ci	$⊢ (Fun F \land A \in dom F) \to (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
3		df-dfat	$⊢ F defAt A \leftrightarrow (A \in dom F \land Fun ({F ↾}_{\{A\}}))$
4	2 3	sylibr	$⊢ (Fun F \land A \in dom F) \to F defAt A$