Metamath Proof Explorer


Theorem relexp0rel

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

Ref Expression
Assertion relexp0rel RVRelRr0

Proof

Step Hyp Ref Expression
1 relres RelIdomRranR
2 relexp0g RVRr0=IdomRranR
3 2 releqd RVRelRr0RelIdomRranR
4 1 3 mpbiri RVRelRr0