Metamath Proof Explorer


Theorem ofc12

Description: Function operation on two constant functions. (Contributed by Mario Carneiro, 28-Jul-2014)

Ref Expression
Hypotheses ofc12.1 φ A V
ofc12.2 φ B W
ofc12.3 φ C X
Assertion ofc12 φ A × B R f A × C = A × B R C

Proof

Step Hyp Ref Expression
1 ofc12.1 φ A V
2 ofc12.2 φ B W
3 ofc12.3 φ C X
4 2 adantr φ x A B W
5 3 adantr φ x A C X
6 fconstmpt A × B = x A B
7 6 a1i φ A × B = x A B
8 fconstmpt A × C = x A C
9 8 a1i φ A × C = x A C
10 1 4 5 7 9 offval2 φ A × B R f A × C = x A B R C
11 fconstmpt A × B R C = x A B R C
12 10 11 eqtr4di φ A × B R f A × C = A × B R C