Metamath Proof Explorer

Theorem rnnonrel

Description: The range of the non-relation part of a class is empty. (Contributed by RP, 22-Oct-2020)

Ref Expression
Assertion rnnonrel 
|- ran ( A \ `' `' A ) = (/)

Proof

Step Hyp Ref Expression
1 dmnonrel 
 |-  dom ( A \ `' `' A ) = (/)
2 dm0rn0 
 |-  ( dom ( A \ `' `' A ) = (/) <-> ran ( A \ `' `' A ) = (/) )
3 1 2 mpbi 
 |-  ran ( A \ `' `' A ) = (/)