Metamath Proof Explorer

Theorem fmpttd

Description: Version of fmptd with inlined definition. Domain and codomain of the mapping operation; deduction form. (Contributed by Glauco Siliprandi, 23-Oct-2021) (Proof shortened by BJ, 16-Aug-2022)

Ref Expression
Hypothesis fmpttd.1 φ x A B C
Assertion fmpttd φ x A B : A C


Step Hyp Ref Expression
1 fmpttd.1 φ x A B C
2 eqid x A B = x A B
3 1 2 fmptd φ x A B : A C