Theorem caofref

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

	Ref	Expression
Hypotheses	caofref.1	|- ( ph -> A e. V )
	caofref.2	|- ( ph -> F : A --> S )
	caofref.3	|- ( ( ph /\ x e. S ) -> x R x )
Assertion	caofref	|- ( ph -> F oR R F )

Proof

Step	Hyp	Ref	Expression
1		caofref.1	|- ( ph -> A e. V )
2		caofref.2	|- ( ph -> F : A --> S )
3		caofref.3	|- ( ( ph /\ x e. S ) -> x R x )
4		id	|- ( x = ( F ` w ) -> x = ( F ` w ) )
5	4 4	breq12d	|- ( x = ( F ` w ) -> ( x R x <-> ( F ` w ) R ( F ` w ) ) )
6	3	ralrimiva	|- ( ph -> A. x e. S x R x )
7	6	adantr	|- ( ( ph /\ w e. A ) -> A. x e. S x R x )
8	2	ffvelrnda	|- ( ( ph /\ w e. A ) -> ( F ` w ) e. S )
9	5 7 8	rspcdva	|- ( ( ph /\ w e. A ) -> ( F ` w ) R ( F ` w ) )
10	9	ralrimiva	|- ( ph -> A. w e. A ( F ` w ) R ( F ` w ) )
11	2	ffnd	|- ( ph -> F Fn A )
12		inidm	|- ( A i^i A ) = A
13		eqidd	|- ( ( ph /\ w e. A ) -> ( F ` w ) = ( F ` w ) )
14	11 11 1 1 12 13 13	ofrfval	|- ( ph -> ( F oR R F <-> A. w e. A ( F ` w ) R ( F ` w ) ) )
15	10 14	mpbird	|- ( ph -> F oR R F )