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 
|- ( R e. V -> Rel ( R ^r 0 ) )

Proof

Step Hyp Ref Expression
1 relres 
 |-  Rel ( _I |` ( dom R u. ran R ) )
2 relexp0g 
 |-  ( R e. V -> ( R ^r 0 ) = ( _I |` ( dom R u. ran R ) ) )
3 2 releqd 
 |-  ( R e. V -> ( Rel ( R ^r 0 ) <-> Rel ( _I |` ( dom R u. ran R ) ) ) )
4 1 3 mpbiri 
 |-  ( R e. V -> Rel ( R ^r 0 ) )