caofid0r

Description: Transfer a right 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		caofid0r.5	$⊢ (φ \land x \in S) \to x R B = x$
5	2	ffnd	$⊢ φ \to F Fn A$
6		fnconstg	$⊢ B \in W \to (A \times \{B\}) Fn A$
7	3 6	syl	$⊢ φ \to (A \times \{B\}) Fn A$
8		eqidd	$⊢ (φ \land w \in A) \to F (w) = F (w)$
9		fvconst2g	$⊢ (B \in W \land w \in A) \to (A \times \{B\}) (w) = B$
10	3 9	sylan	$⊢ (φ \land w \in A) \to (A \times \{B\}) (w) = B$
11	4	ralrimiva	$⊢ φ \to \forall x \in S x R B = x$
12	2	ffvelcdmda	$⊢ (φ \land w \in A) \to F (w) \in S$
13		oveq1	$⊢ x = F (w) \to x R B = F (w) R B$
14		id	$⊢ x = F (w) \to x = F (w)$
15	13 14	eqeq12d	$⊢ x = F (w) \to (x R B = x \leftrightarrow F (w) R B = F (w))$
16	15	rspccva	$⊢ (\forall x \in S x R B = x \land F (w) \in S) \to F (w) R B = F (w)$
17	11 12 16	syl2an2r	$⊢ (φ \land w \in A) \to F (w) R B = F (w)$
18	1 5 7 5 8 10 17	offveq	$⊢ φ \to F R_{f} (A \times \{B\}) = F$

Metamath Proof Explorer