Metamath Proof Explorer

Theorem cnveqi

Description: Equality inference for converse relation. (Contributed by NM, 23-Dec-2008)

Ref Expression
Hypothesis cnveqi.1 ⊢ 𝐴 = 𝐵
Assertion cnveqi ◡ 𝐴 = ◡ 𝐵

Proof

Step Hyp Ref Expression
1 cnveqi.1 ⊢ 𝐴 = 𝐵
2 cnveq ⊢ ( 𝐴 = 𝐵 → ◡ 𝐴 = ◡ 𝐵 )
3 1 2 ax-mp ⊢ ◡ 𝐴 = ◡ 𝐵