Metamath Proof Explorer


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 ) )