Theorem funmpt2

Description: Functionality of a class given by a maps-to notation. (Contributed by FL, 17-Feb-2008) (Revised by Mario Carneiro, 31-May-2014)

	Ref	Expression
Hypothesis	funmpt2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
Assertion	funmpt2	⊢ Fun 𝐹

Proof

Step	Hyp	Ref	Expression
1		funmpt2.1	⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2		funmpt	⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
3	1	funeqi	⊢ ( Fun 𝐹 ↔ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
4	2 3	mpbir	⊢ Fun 𝐹