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