Theorem funmpt

Description: A function in maps-to notation is a function. (Contributed by Mario Carneiro, 13-Jan-2013)

	Ref	Expression
Assertion	funmpt	⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		funopab4	⊢ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
2		df-mpt	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) }
3	2	funeqi	⊢ ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ↔ Fun { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵 ) } )
4	1 3	mpbir	⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 )