Metamath Proof Explorer

Theorem fvconst2

Description: The value of a constant function. (Contributed by NM, 16-Apr-2005)

Ref Expression
Hypothesis fvconst2.1 B V
Assertion fvconst2 C A A × B C = B


Step Hyp Ref Expression
1 fvconst2.1 B V
2 fvconst2g B V C A A × B C = B
3 1 2 mpan C A A × B C = B