Metamath Proof Explorer

Theorem fnmpti

Description: Functionality and domain of an ordered-pair class abstraction. (Contributed by NM, 29-Jan-2004) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses fnmpti.1 B V
fnmpti.2 F = x A B
Assertion fnmpti F Fn A


Step Hyp Ref Expression
1 fnmpti.1 B V
2 fnmpti.2 F = x A B
3 1 rgenw x A B V
4 2 mptfng x A B V F Fn A
5 3 4 mpbi F Fn A