Metamath Proof Explorer

Theorem cnveqb

Description: Equality theorem for converse. (Contributed by FL, 19-Sep-2011)

Ref Expression
Assertion cnveqb ⊢ Rel ⁡ A ∧ Rel ⁡ B → A = B ↔ A -1 = B -1

Proof

Step Hyp Ref Expression
1 cnveq ⊢ A = B → A -1 = B -1
2 dfrel2 ⊢ Rel ⁡ A ↔ A -1 -1 = A
3 dfrel2 ⊢ Rel ⁡ B ↔ B -1 -1 = B
4 cnveq ⊢ A -1 = B -1 → A -1 -1 = B -1 -1
5 eqeq2 ⊢ B = B -1 -1 → A -1 -1 = B ↔ A -1 -1 = B -1 -1
6 4 5 syl5ibr ⊢ B = B -1 -1 → A -1 = B -1 → A -1 -1 = B
7 6 eqcoms ⊢ B -1 -1 = B → A -1 = B -1 → A -1 -1 = B
8 3 7 sylbi ⊢ Rel ⁡ B → A -1 = B -1 → A -1 -1 = B
9 eqeq1 ⊢ A = A -1 -1 → A = B ↔ A -1 -1 = B
10 9 imbi2d ⊢ A = A -1 -1 → A -1 = B -1 → A = B ↔ A -1 = B -1 → A -1 -1 = B
11 8 10 syl5ibr ⊢ A = A -1 -1 → Rel ⁡ B → A -1 = B -1 → A = B
12 11 eqcoms ⊢ A -1 -1 = A → Rel ⁡ B → A -1 = B -1 → A = B
13 2 12 sylbi ⊢ Rel ⁡ A → Rel ⁡ B → A -1 = B -1 → A = B
14 13 imp ⊢ Rel ⁡ A ∧ Rel ⁡ B → A -1 = B -1 → A = B
15 1 14 impbid2 ⊢ Rel ⁡ A ∧ Rel ⁡ B → A = B ↔ A -1 = B -1