Metamath Proof Explorer

Theorem fvconst2g

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

Ref Expression
Assertion fvconst2g B D C A A × B C = B


Step Hyp Ref Expression
1 fconstg B D A × B : A B
2 fvconst A × B : A B C A A × B C = B
3 1 2 sylan B D C A A × B C = B