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	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) → Fun 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		elpmi	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) → ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) )
2		ffun	⊢ ( 𝐹 : dom 𝐹 ⟶ 𝐴 → Fun 𝐹 )
3	2	adantr	⊢ ( ( 𝐹 : dom 𝐹 ⟶ 𝐴 ∧ dom 𝐹 ⊆ 𝐵 ) → Fun 𝐹 )
4	1 3	syl	⊢ ( 𝐹 ∈ ( 𝐴 ↑pm 𝐵 ) → Fun 𝐹 )