Metamath Proof Explorer

Theorem dmnonrel

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

Ref Expression
Assertion dmnonrel 
|- dom ( A \ `' `' A ) = (/)

Proof

Step Hyp Ref Expression
1 dfdm4 
 |-  dom ( A \ `' `' A ) = ran `' ( A \ `' `' A )
2 cnvnonrel 
 |-  `' ( A \ `' `' A ) = (/)
3 2 rneqi 
 |-  ran `' ( A \ `' `' A ) = ran (/)
4 rn0 
 |-  ran (/) = (/)
5 1 3 4 3eqtri 
 |-  dom ( A \ `' `' A ) = (/)