Metamath Proof Explorer

Theorem imanonrel

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

Ref Expression
Assertion imanonrel 
|- ( ( A \ `' `' A ) " B ) = (/)

Proof

Step Hyp Ref Expression
1 df-ima 
 |-  ( ( A \ `' `' A ) " B ) = ran ( ( A \ `' `' A ) |` B )
2 resnonrel 
 |-  ( ( A \ `' `' A ) |` B ) = (/)
3 2 rneqi 
 |-  ran ( ( A \ `' `' A ) |` B ) = ran (/)
4 rn0 
 |-  ran (/) = (/)
5 1 3 4 3eqtri 
 |-  ( ( A \ `' `' A ) " B ) = (/)