Theorem dfid5

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

	Ref	Expression
Assertion	dfid5	$$⊢\mathrm{I}=\left(x\in \mathrm{V}⟼x{\uparrow }_{r}1\right)$$

Proof

Step	Hyp	Ref	Expression
1		dfid4	$$⊢\mathrm{I}=\left(x\in \mathrm{V}⟼x\right)$$
2		relexp1g	$$⊢x\in \mathrm{V}\to x{\uparrow }_{r}1=x$$
3	2	mpteq2ia	$$⊢\left(x\in \mathrm{V}⟼x{\uparrow }_{r}1\right)=\left(x\in \mathrm{V}⟼x\right)$$
4	1 3	eqtr4i	$$⊢\mathrm{I}=\left(x\in \mathrm{V}⟼x{\uparrow }_{r}1\right)$$