Theorem relexp0rel

Description: The exponentiation of a class to zero is a relation. (Contributed by RP, 23-May-2020)

	Ref	Expression
Assertion	relexp0rel	$$⊢R\in V\to \mathrm{Rel}\left(R{\uparrow }_{r}0\right)$$

Proof

Step	Hyp	Ref	Expression
1		relres	$$⊢\mathrm{Rel}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}\right)$$
2		relexp0g	$$⊢R\in V\to R{\uparrow }_{r}0={\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}$$
3	2	releqd	$$⊢R\in V\to \left(\mathrm{Rel}\left(R{\uparrow }_{r}0\right)\leftrightarrow \mathrm{Rel}\left({\mathrm{I}\upharpoonright }_{\left(\mathrm{dom}R\cup \mathrm{ran}R\right)}\right)\right)$$
4	1 3	mpbiri	$$⊢R\in V\to \mathrm{Rel}\left(R{\uparrow }_{r}0\right)$$