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 ⊢ ( 𝐴 = 𝐵 → ◡ 𝐴 = ◡ 𝐵 )