Theorem fmpt3d

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Thierry Arnoux, 4-Jun-2017)

	Ref	Expression
Hypotheses	fmpt3d.1	|- ( ph -> F = ( x e. A |-> B ) )
	fmpt3d.2	|- ( ( ph /\ x e. A ) -> B e. C )
Assertion	fmpt3d	|- ( ph -> F : A --> C )

Proof

Step	Hyp	Ref	Expression
1		fmpt3d.1	|- ( ph -> F = ( x e. A |-> B ) )
2		fmpt3d.2	|- ( ( ph /\ x e. A ) -> B e. C )
3	2	fmpttd	|- ( ph -> ( x e. A |-> B ) : A --> C )
4	1	feq1d	|- ( ph -> ( F : A --> C <-> ( x e. A |-> B ) : A --> C ) )
5	3 4	mpbird	|- ( ph -> F : A --> C )