Theorem ofc12

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

	Ref	Expression
Hypotheses	ofc12.1	$$⊢\phi \to A\in V$$
	ofc12.2	$$⊢\phi \to B\in W$$
	ofc12.3	$$⊢\phi \to C\in X$$
Assertion	ofc12	$$⊢\phi \to \left(A\times \left\{B\right\}\right)R_f\left(A\times \left\{C\right\}\right)=A\times \left\{BRC\right\}$$

Proof

Step	Hyp	Ref	Expression
1		ofc12.1	$$⊢\phi \to A\in V$$
2		ofc12.2	$$⊢\phi \to B\in W$$
3		ofc12.3	$$⊢\phi \to C\in X$$
4	2	adantr	$$⊢\left(\phi \wedge x\in A\right)\to B\in W$$
5	3	adantr	$$⊢\left(\phi \wedge x\in A\right)\to C\in X$$
6		fconstmpt	$$⊢A\times \left\{B\right\}=\left(x\in A⟼B\right)$$
7	6	a1i	$$⊢\phi \to A\times \left\{B\right\}=\left(x\in A⟼B\right)$$
8		fconstmpt	$$⊢A\times \left\{C\right\}=\left(x\in A⟼C\right)$$
9	8	a1i	$$⊢\phi \to A\times \left\{C\right\}=\left(x\in A⟼C\right)$$
10	1 4 5 7 9	offval2	$$⊢\phi \to \left(A\times \left\{B\right\}\right)R_f\left(A\times \left\{C\right\}\right)=\left(x\in A⟼BRC\right)$$
11		fconstmpt	$$⊢A\times \left\{BRC\right\}=\left(x\in A⟼BRC\right)$$
12	10 11	eqtr4di	$$⊢\phi \to \left(A\times \left\{B\right\}\right)R_f\left(A\times \left\{C\right\}\right)=A\times \left\{BRC\right\}$$