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		cnvssb	⊢ ( Rel 𝐴 → ( 𝐴 ⊆ 𝐵 ↔ ◡ 𝐴 ⊆ ◡ 𝐵 ) )
2		cnvssb	⊢ ( Rel 𝐵 → ( 𝐵 ⊆ 𝐴 ↔ ◡ 𝐵 ⊆ ◡ 𝐴 ) )
3	1 2	bi2anan9	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) ↔ ( ◡ 𝐴 ⊆ ◡ 𝐵 ∧ ◡ 𝐵 ⊆ ◡ 𝐴 ) ) )
4		eqss	⊢ ( 𝐴 = 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ⊆ 𝐴 ) )
5		eqss	⊢ ( ◡ 𝐴 = ◡ 𝐵 ↔ ( ◡ 𝐴 ⊆ ◡ 𝐵 ∧ ◡ 𝐵 ⊆ ◡ 𝐴 ) )
6	3 4 5	3bitr4g	⊢ ( ( Rel 𝐴 ∧ Rel 𝐵 ) → ( 𝐴 = 𝐵 ↔ ◡ 𝐴 = ◡ 𝐵 ) )