Metamath Proof Explorer


Theorem fmptd

Description: Domain and codomain of the mapping operation; deduction form. (Contributed by Mario Carneiro, 13-Jan-2013)

Ref Expression
Hypotheses fmptd.1 φxABC
fmptd.2 F=xAB
Assertion fmptd φF:AC

Proof

Step Hyp Ref Expression
1 fmptd.1 φxABC
2 fmptd.2 F=xAB
3 1 ralrimiva φxABC
4 2 fmpt xABCF:AC
5 3 4 sylib φF:AC