Metamath Proof Explorer


Theorem fmpti

Description: Functionality of the mapping operation. (Contributed by NM, 19-Mar-2005) (Revised by Mario Carneiro, 1-Sep-2015)

Ref Expression
Hypotheses fmpt.1 F = x A C
fmpti.2 x A C B
Assertion fmpti F : A B

Proof

Step Hyp Ref Expression
1 fmpt.1 F = x A C
2 fmpti.2 x A C B
3 2 rgen x A C B
4 1 fmpt x A C B F : A B
5 3 4 mpbi F : A B