This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnveq0

Description: A relation 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 cnv0 
 |-  `' (/) = (/)
2 rel0 
 |-  Rel (/)
3 cnveqb 
 |-  ( ( Rel A /\ Rel (/) ) -> ( A = (/) <-> `' A = `' (/) ) )
4 2 3 mpan2 
 |-  ( Rel A -> ( A = (/) <-> `' A = `' (/) ) )
5 eqeq2 
 |-  ( (/) = `' (/) -> ( `' A = (/) <-> `' A = `' (/) ) )
6 5 bibi2d 
 |-  ( (/) = `' (/) -> ( ( A = (/) <-> `' A = (/) ) <-> ( A = (/) <-> `' A = `' (/) ) ) )
7 4 6 imbitrrid 
 |-  ( (/) = `' (/) -> ( Rel A -> ( A = (/) <-> `' A = (/) ) ) )
8 7 eqcoms 
 |-  ( `' (/) = (/) -> ( Rel A -> ( A = (/) <-> `' A = (/) ) ) )
9 1 8 ax-mp 
 |-  ( Rel A -> ( A = (/) <-> `' A = (/) ) )