Define "log using an arbitrary base" function and then prove some of its properties. Note that is generalized to an arbitrary base and arbitrary parameter in , but it doesn't accept infinities as arguments, unlike .
Metamath doesn't care what letters are used to represent classes. Usually classes begin with the letter "A", but here we use "B" and "X" to more clearly distinguish between "base" and "other parameter of log".
There are different ways this could be defined in Metamath. The approach used here is intentionally similar to existing 2-parameter Metamath functions (operations): where is the base and is the argument of the logarithm function. An alternative would be to support the notational form ; that looks a little more like traditional notation. Such a function for a fixed base can be obtained in Metamath (without the need for a new definition) by the curry function: , see logbmpt, logbf and logbfval.