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