Metamath Proof Explorer


Theorem mpofun

Description: The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012) (Proof shortened by SN, 23-Jul-2024)

Ref Expression
Hypothesis mpofun.1 F = x A , y B C
Assertion mpofun Fun F

Proof

Step Hyp Ref Expression
1 mpofun.1 F = x A , y B C
2 moeq * z z = C
3 2 moani * z x A y B z = C
4 3 funoprab Fun x y z | x A y B z = C
5 df-mpo x A , y B C = x y z | x A y B z = C
6 1 5 eqtri F = x y z | x A y B z = C
7 6 funeqi Fun F Fun x y z | x A y B z = C
8 4 7 mpbir Fun F