Metamath Proof Explorer


Theorem cnveq

Description: Equality theorem for converse relation. (Contributed by NM, 13-Aug-1995)

Ref Expression
Assertion cnveq ( 𝐴 = 𝐵 𝐴 = 𝐵 )

Proof

Step Hyp Ref Expression
1 cnvss ( 𝐴𝐵 𝐴 𝐵 )
2 cnvss ( 𝐵𝐴 𝐵 𝐴 )
3 1 2 anim12i ( ( 𝐴𝐵𝐵𝐴 ) → ( 𝐴 𝐵 𝐵 𝐴 ) )
4 eqss ( 𝐴 = 𝐵 ↔ ( 𝐴𝐵𝐵𝐴 ) )
5 eqss ( 𝐴 = 𝐵 ↔ ( 𝐴 𝐵 𝐵 𝐴 ) )
6 3 4 5 3imtr4i ( 𝐴 = 𝐵 𝐴 = 𝐵 )