Theorem idrval

Description: The value of the identity element. (Contributed by FL, 12-Dec-2009) (Revised by Mario Carneiro, 22-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	idrval.1	|- X = ran G
	idrval.2	|- U = ( GId ` G )
Assertion	idrval	|- ( G e. A -> U = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )

Proof

Step	Hyp	Ref	Expression
1		idrval.1	|- X = ran G
2		idrval.2	|- U = ( GId ` G )
3	1	gidval	|- ( G e. A -> ( GId ` G ) = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )
4	2 3	syl5eq	|- ( G e. A -> U = ( iota_ u e. X A. x e. X ( ( u G x ) = x /\ ( x G u ) = x ) ) )