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 -1 = ∅

Proof

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