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	syl5ibr	|- ( (/) = `' (/) -> ( Rel A -> ( A = (/) <-> `' A = (/) ) ) )
8	7	eqcoms	|- ( `' (/) = (/) -> ( Rel A -> ( A = (/) <-> `' A = (/) ) ) )
9	1 8	ax-mp	|- ( Rel A -> ( A = (/) <-> `' A = (/) ) )