Theorem caofref

Description: Transfer a reflexive law to the function relation. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	caofref.1	$$⊢\phi \to A\in V$$
	caofref.2	$$⊢\phi \to F:A⟶S$$
	caofref.3	$$⊢\left(\phi \wedge x\in S\right)\to xRx$$
Assertion	caofref	$$⊢\phi \to F{R}_{f}F$$

Proof

Step	Hyp	Ref	Expression
1		caofref.1	$$⊢\phi \to A\in V$$
2		caofref.2	$$⊢\phi \to F:A⟶S$$
3		caofref.3	$$⊢\left(\phi \wedge x\in S\right)\to xRx$$
4		id	$$⊢x=F\left(w\right)\to x=F\left(w\right)$$
5	4 4	breq12d	$$⊢x=F\left(w\right)\to \left(xRx\leftrightarrow F\left(w\right)RF\left(w\right)\right)$$
6	3	ralrimiva	$$⊢\phi \to \forall x\in SxRx$$
7	6	adantr	$$⊢\left(\phi \wedge w\in A\right)\to \forall x\in SxRx$$
8	2	ffvelrnda	$$⊢\left(\phi \wedge w\in A\right)\to F\left(w\right)\in S$$
9	5 7 8	rspcdva	$$⊢\left(\phi \wedge w\in A\right)\to F\left(w\right)RF\left(w\right)$$
10	9	ralrimiva	$$⊢\phi \to \forall w\in AF\left(w\right)RF\left(w\right)$$
11	2	ffnd	$$⊢\phi \to FFnA$$
12		inidm	$$⊢A\cap A=A$$
13		eqidd	$$⊢\left(\phi \wedge w\in A\right)\to F\left(w\right)=F\left(w\right)$$
14	11 11 1 1 12 13 13	ofrfval	$$⊢\phi \to \left(F{R}_{f}F\leftrightarrow \forall w\in AF\left(w\right)RF\left(w\right)\right)$$
15	10 14	mpbird	$$⊢\phi \to F{R}_{f}F$$