Theorem fmptd2f

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step	Hyp	Ref	Expression
1		fmptd2f.1	$$⊢Ⅎx\phi$$
2		fmptd2f.2	$$⊢\left(\phi \wedge x\in A\right)\to B\in C$$
3		eqid	$$⊢\left(x\in A⟼B\right)=\left(x\in A⟼B\right)$$
4	1 2 3	fmptdf	$$⊢\phi \to \left(x\in A⟼B\right):A⟶C$$