ofc2

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

Step	Hyp	Ref	Expression
1		ofc2.1	$⊢ φ \to A \in V$
2		ofc2.2	$⊢ φ \to B \in W$
3		ofc2.3	$⊢ φ \to F Fn A$
4		ofc2.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	3 6 1 1 7 4 9	ofval	$⊢ (φ \land X \in A) \to (F R_{f} (A \times \{B\})) (X) = C R B$

Metamath Proof Explorer