Metamath Proof Explorer

Theorem cnveq0

Description: A relation is empty iff its converse is empty. (Contributed by FL, 19-Sep-2011)

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

Proof

Step Hyp Ref Expression
1 rel0 
 |-  Rel (/)
2 cnveqb 
 |-  ( ( Rel A /\ Rel (/) ) -> ( A = (/) <-> `' A = `' (/) ) )
3 1 2 mpan2 
 |-  ( Rel A -> ( A = (/) <-> `' A = `' (/) ) )
4 cnv0 
 |-  `' (/) = (/)
5 4 eqeq2i 
 |-  ( `' A = `' (/) <-> `' A = (/) )
6 3 5 bitrdi 
 |-  ( Rel A -> ( A = (/) <-> `' A = (/) ) )