caofid0l

Description: Transfer a left identity law to the function operation. (Contributed by NM, 21-Oct-2014)

Step	Hyp	Ref	Expression
1		caofref.1	$⊢ φ \to A \in V$
2		caofref.2	$⊢ φ \to F : A ⟶ S$
3		caofid0.3	$⊢ φ \to B \in W$
4		caofid0l.5	$⊢ (φ \land x \in S) \to B R x = x$
5		fnconstg	$⊢ B \in W \to (A \times \{B\}) Fn A$
6	3 5	syl	$⊢ φ \to (A \times \{B\}) Fn A$
7	2	ffnd	$⊢ φ \to F Fn A$
8		fvconst2g	$⊢ (B \in W \land w \in A) \to (A \times \{B\}) (w) = B$
9	3 8	sylan	$⊢ (φ \land w \in A) \to (A \times \{B\}) (w) = B$
10		eqidd	$⊢ (φ \land w \in A) \to F (w) = F (w)$
11	4	ralrimiva	$⊢ φ \to \forall x \in S B R x = x$
12	2	ffvelcdmda	$⊢ (φ \land w \in A) \to F (w) \in S$
13		oveq2	$⊢ x = F (w) \to B R x = B R F (w)$
14		id	$⊢ x = F (w) \to x = F (w)$
15	13 14	eqeq12d	$⊢ x = F (w) \to (B R x = x \leftrightarrow B R F (w) = F (w))$
16	15	rspccva	$⊢ (\forall x \in S B R x = x \land F (w) \in S) \to B R F (w) = F (w)$
17	11 12 16	syl2an2r	$⊢ (φ \land w \in A) \to B R F (w) = F (w)$
18	1 6 7 7 9 10 17	offveq	$⊢ φ \to (A \times \{B\}) R_{f} F = F$

Metamath Proof Explorer