This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cnveqb

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

Ref Expression
Assertion cnveqb ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ◡ 𝐴 = ◡ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 cnveq ⊢ ( 𝐴 = 𝐵 → ◡ 𝐴 = ◡ 𝐵 )
2 dfrel2 ⊢ ( Rel 𝐴 ↔ ◡ ◡ 𝐴 = 𝐴 )
3 dfrel2 ⊢ ( Rel 𝐵 ↔ ◡ ◡ 𝐵 = 𝐵 )
4 cnveq ⊢ ( ◡ 𝐴 = ◡ 𝐵 → ◡ ◡ 𝐴 = ◡ ◡ 𝐵 )
5 eqeq2 ⊢ ( 𝐵 = ◡ ◡ 𝐵 → ( ◡ ◡ 𝐴 = 𝐵 ↔ ◡ ◡ 𝐴 = ◡ ◡ 𝐵 ) )
6 4 5 imbitrrid ⊢ ( 𝐵 = ◡ ◡ 𝐵 → ( ◡ 𝐴 = ◡ 𝐵 → ◡ ◡ 𝐴 = 𝐵 ) )
7 6 eqcoms ⊢ ( ◡ ◡ 𝐵 = 𝐵 → ( ◡ 𝐴 = ◡ 𝐵 → ◡ ◡ 𝐴 = 𝐵 ) )
8 3 7 sylbi ⊢ ( Rel 𝐵 → ( ◡ 𝐴 = ◡ 𝐵 → ◡ ◡ 𝐴 = 𝐵 ) )
9 eqeq1 ⊢ ( 𝐴 = ◡ ◡ 𝐴 → ( 𝐴 = 𝐵 ↔ ◡ ◡ 𝐴 = 𝐵 ) )
10 9 imbi2d ⊢ ( 𝐴 = ◡ ◡ 𝐴 → ( ( ◡ 𝐴 = ◡ 𝐵 → 𝐴 = 𝐵 ) ↔ ( ◡ 𝐴 = ◡ 𝐵 → ◡ ◡ 𝐴 = 𝐵 ) ) )
11 8 10 imbitrrid ⊢ ( 𝐴 = ◡ ◡ 𝐴 → ( Rel 𝐵 → ( ◡ 𝐴 = ◡ 𝐵 → 𝐴 = 𝐵 ) ) )
12 11 eqcoms ⊢ ( ◡ ◡ 𝐴 = 𝐴 → ( Rel 𝐵 → ( ◡ 𝐴 = ◡ 𝐵 → 𝐴 = 𝐵 ) ) )
13 2 12 sylbi ⊢ ( Rel 𝐴 → ( Rel 𝐵 → ( ◡ 𝐴 = ◡ 𝐵 → 𝐴 = 𝐵 ) ) )
14 13 imp ⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( ◡ 𝐴 = ◡ 𝐵 → 𝐴 = 𝐵 ) )
15 1 14 impbid2 ⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ◡ 𝐴 = ◡ 𝐵 ) )