Metamath Proof Explorer

Theorem pmfun

Description: A partial function is a function. (Contributed by Mario Carneiro, 30-Jan-2014) (Revised by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	pmfun	$⊢ F \in (A ↑_{𝑝𝑚} B) \to Fun F$

Step	Hyp	Ref	Expression
1		elpmi	$⊢ F \in (A ↑_{𝑝𝑚} B) \to (F : dom F ⟶ A \land dom F \subseteq B)$
2		ffun	$⊢ F : dom F ⟶ A \to Fun F$
3	2	adantr	$⊢ (F : dom F ⟶ A \land dom F \subseteq B) \to Fun F$
4	1 3	syl	$⊢ F \in (A ↑_{𝑝𝑚} B) \to Fun F$