Theorem relexp0rel

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

	Ref	Expression
Assertion	relexp0rel	⊢ ( 𝑅 ∈ 𝑉 → Rel ( 𝑅 ↑𝑟 0 ) )

Proof

Step	Hyp	Ref	Expression
1		relres	⊢ Rel ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) )
2		relexp0g	⊢ ( 𝑅 ∈ 𝑉 → ( 𝑅 ↑𝑟 0 ) = ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) )
3	2	releqd	⊢ ( 𝑅 ∈ 𝑉 → ( Rel ( 𝑅 ↑𝑟 0 ) ↔ Rel ( I ↾ ( dom 𝑅 ∪ ran 𝑅 ) ) ) )
4	1 3	mpbiri	⊢ ( 𝑅 ∈ 𝑉 → Rel ( 𝑅 ↑𝑟 0 ) )