Theorem fmpt3d

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

	Ref	Expression
Hypotheses	fmpt3d.1	$$⊢\phi \to F=\left(x\in A⟼B\right)$$
	fmpt3d.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
Assertion	fmpt3d	$$⊢\phi \to F:A⟶C$$

Proof

Step	Hyp	Ref	Expression
1		fmpt3d.1	$$⊢\phi \to F=\left(x\in A⟼B\right)$$
2		fmpt3d.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
3	2	fmpttd	$$⊢\phi \to \left(x\in A⟼B\right):A⟶C$$
4	1	feq1d	$$⊢\phi \to \left(F:A⟶C\leftrightarrow \left(x\in A⟼B\right):A⟶C\right)$$
5	3 4	mpbird	$$⊢\phi \to F:A⟶C$$