Metamath Proof Explorer

Theorem cnvnonrel

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

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

Proof

Step Hyp Ref Expression
1 cnvdif 
 |-  `' ( A \ `' `' A ) = ( `' A \ `' `' `' A )
2 relcnv 
 |-  Rel `' A
3 relnonrel 
 |-  ( Rel `' A <-> ( `' A \ `' `' `' A ) = (/) )
4 2 3 mpbi 
 |-  ( `' A \ `' `' `' A ) = (/)
5 1 4 eqtri 
 |-  `' ( A \ `' `' A ) = (/)