Theorem cnveq0

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

	Ref	Expression
Assertion	cnveq0	⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ ◡ 𝐴 = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		rel0	⊢ Rel ∅
2		cnveqb	⊢ ( ( Rel 𝐴 ∧ Rel ∅ ) → ( 𝐴 = ∅ ↔ ◡ 𝐴 = ◡ ∅ ) )
3	1 2	mpan2	⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ ◡ 𝐴 = ◡ ∅ ) )
4		cnv0	⊢ ◡ ∅ = ∅
5	4	eqeq2i	⊢ ( ◡ 𝐴 = ◡ ∅ ↔ ◡ 𝐴 = ∅ )
6	3 5	bitrdi	⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ ◡ 𝐴 = ∅ ) )