Theorem cnveq0

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

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

Proof

Step	Hyp	Ref	Expression
1		cnv0	⊢ ◡ ∅ = ∅
2		rel0	⊢ Rel ∅
3		cnveqb	⊢ ( ( Rel 𝐴 ∧ Rel ∅ ) → ( 𝐴 = ∅ ↔ ◡ 𝐴 = ◡ ∅ ) )
4	2 3	mpan2	⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ ◡ 𝐴 = ◡ ∅ ) )
5		eqeq2	⊢ ( ∅ = ◡ ∅ → ( ◡ 𝐴 = ∅ ↔ ◡ 𝐴 = ◡ ∅ ) )
6	5	bibi2d	⊢ ( ∅ = ◡ ∅ → ( ( 𝐴 = ∅ ↔ ◡ 𝐴 = ∅ ) ↔ ( 𝐴 = ∅ ↔ ◡ 𝐴 = ◡ ∅ ) ) )
7	4 6	imbitrrid	⊢ ( ∅ = ◡ ∅ → ( Rel 𝐴 → ( 𝐴 = ∅ ↔ ◡ 𝐴 = ∅ ) ) )
8	7	eqcoms	⊢ ( ◡ ∅ = ∅ → ( Rel 𝐴 → ( 𝐴 = ∅ ↔ ◡ 𝐴 = ∅ ) ) )
9	1 8	ax-mp	⊢ ( Rel 𝐴 → ( 𝐴 = ∅ ↔ ◡ 𝐴 = ∅ ) )