Metamath Proof Explorer

Theorem cnveq0b

Description: A class is empty iff it is a relation whose converse is empty. (Contributed by SN, 8-Oct-2026)

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

Proof

Step Hyp Ref Expression
1 rel0 
 |-  Rel (/)
2 releq 
 |-  ( A = (/) -> ( Rel A <-> Rel (/) ) )
3 1 2 mpbiri 
 |-  ( A = (/) -> Rel A )
4 cnveq0 
 |-  ( Rel A -> ( A = (/) <-> `' A = (/) ) )
5 3 4 biadanii 
 |-  ( A = (/) <-> ( Rel A /\ `' A = (/) ) )