Theorem idfu1

Description: Value of the object part of the identity functor. (Contributed by Mario Carneiro, 3-Jan-2017)

	Ref	Expression
Hypotheses	idfuval.i	|- I = ( idFunc ` C )
	idfuval.b	|- B = ( Base ` C )
	idfuval.c	|- ( ph -> C e. Cat )
	idfu1.x	|- ( ph -> X e. B )
Assertion	idfu1	|- ( ph -> ( ( 1st ` I ) ` X ) = X )

Proof

Step	Hyp	Ref	Expression
1		idfuval.i	|- I = ( idFunc ` C )
2		idfuval.b	|- B = ( Base ` C )
3		idfuval.c	|- ( ph -> C e. Cat )
4		idfu1.x	|- ( ph -> X e. B )
5	1 2 3	idfu1st	|- ( ph -> ( 1st ` I ) = ( _I |` B ) )
6	5	fveq1d	|- ( ph -> ( ( 1st ` I ) ` X ) = ( ( _I |` B ) ` X ) )
7		fvresi	|- ( X e. B -> ( ( _I |` B ) ` X ) = X )
8	4 7	syl	|- ( ph -> ( ( _I |` B ) ` X ) = X )
9	6 8	eqtrd	|- ( ph -> ( ( 1st ` I ) ` X ) = X )