Theorem mptfnd

Description: The maps-to notation defines a function with domain. (Contributed by NM, 9-Apr-2013) (Revised by Thierry Arnoux, 10-May-2017)

	Ref	Expression
Hypotheses	mptfnd.1	⊢ Ⅎ 𝑥 𝐴
	mptfnd.2	⊢ Ⅎ 𝑥 𝜑
	mptfnd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
Assertion	mptfnd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		mptfnd.1	⊢ Ⅎ 𝑥 𝐴
2		mptfnd.2	⊢ Ⅎ 𝑥 𝜑
3		mptfnd.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
4	3	ex	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ 𝑉 ) )
5		elex	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ V )
6	4 5	syl6	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 → 𝐵 ∈ V ) )
7	2 6	ralrimi	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V )
8	1	mptfnf	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
9	7 8	sylib	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )