Metamath Proof Explorer

Theorem relnonrel

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

Ref Expression
Assertion relnonrel 
|- ( Rel A <-> ( A \ `' `' A ) = (/) )

Proof

Step Hyp Ref Expression
1 dfrel2 
 |-  ( Rel A <-> `' `' A = A )
2 eqss 
 |-  ( `' `' A = A <-> ( `' `' A C_ A /\ A C_ `' `' A ) )
3 1 2 bitri 
 |-  ( Rel A <-> ( `' `' A C_ A /\ A C_ `' `' A ) )
4 cnvcnvss 
 |-  `' `' A C_ A
5 4 biantrur 
 |-  ( A C_ `' `' A <-> ( `' `' A C_ A /\ A C_ `' `' A ) )
6 ssdif0 
 |-  ( A C_ `' `' A <-> ( A \ `' `' A ) = (/) )
7 3 5 6 3bitr2i 
 |-  ( Rel A <-> ( A \ `' `' A ) = (/) )