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 = ( 𝑥 ∈ V ↦ ( 𝑥 ↑𝑟 1 ) )

Proof

Step	Hyp	Ref	Expression
1		dfid4	⊢ I = ( 𝑥 ∈ V ↦ 𝑥 )
2		relexp1g	⊢ ( 𝑥 ∈ V → ( 𝑥 ↑𝑟 1 ) = 𝑥 )
3	2	mpteq2ia	⊢ ( 𝑥 ∈ V ↦ ( 𝑥 ↑𝑟 1 ) ) = ( 𝑥 ∈ V ↦ 𝑥 )
4	1 3	eqtr4i	⊢ I = ( 𝑥 ∈ V ↦ ( 𝑥 ↑𝑟 1 ) )