ofc1

Description: Left operation by a constant. (Contributed by Mario Carneiro, 24-Jul-2014)

	Ref	Expression
Hypotheses	ofc1.1	$⊢ φ \to A \in V$
	ofc1.2	$⊢ φ \to B \in W$
	ofc1.3	$⊢ φ \to F Fn A$
	ofc1.4	$⊢ (φ \land X \in A) \to F (X) = C$
Assertion	ofc1	$⊢ (φ \land X \in A) \to ((A \times \{B\}) R_{f} F) (X) = B R C$

Step	Hyp	Ref	Expression
1		ofc1.1	$⊢ φ \to A \in V$
2		ofc1.2	$⊢ φ \to B \in W$
3		ofc1.3	$⊢ φ \to F Fn A$
4		ofc1.4	$⊢ (φ \land X \in A) \to F (X) = C$
5		fnconstg	$⊢ B \in W \to (A \times \{B\}) Fn A$
6	2 5	syl	$⊢ φ \to (A \times \{B\}) Fn A$
7		inidm	$⊢ A \cap A = A$
8		fvconst2g	$⊢ (B \in W \land X \in A) \to (A \times \{B\}) (X) = B$
9	2 8	sylan	$⊢ (φ \land X \in A) \to (A \times \{B\}) (X) = B$
10	6 3 1 1 7 9 4	ofval	$⊢ (φ \land X \in A) \to ((A \times \{B\}) R_{f} F) (X) = B R C$

Metamath Proof Explorer