Theorem dfid5

Description: Identity relation is equal to relational exponentiation to the first power. (Contributed by RP, 9-Jun-2020)

	Ref	Expression
Assertion	dfid5	|- _I = ( x e. _V |-> ( x ^r 1 ) )

Proof

Step	Hyp	Ref	Expression
1		dfid4	|- _I = ( x e. _V |-> x )
2		relexp1g	|- ( x e. _V -> ( x ^r 1 ) = x )
3	2	mpteq2ia	|- ( x e. _V |-> ( x ^r 1 ) ) = ( x e. _V |-> x )
4	1 3	eqtr4i	|- _I = ( x e. _V |-> ( x ^r 1 ) )