Theorem brid

Description: Property of the identity binary relation. (Contributed by Peter Mazsa, 18-Dec-2021)

	Ref	Expression
Assertion	brid	⊢ ( 𝐴 I 𝐵 ↔ 𝐵 I 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cnvi	⊢ ◡ I = I
2	1	breqi	⊢ ( 𝐴 ◡ I 𝐵 ↔ 𝐴 I 𝐵 )
3		reli	⊢ Rel I
4	3	relbrcnv	⊢ ( 𝐴 ◡ I 𝐵 ↔ 𝐵 I 𝐴 )
5	2 4	bitr3i	⊢ ( 𝐴 I 𝐵 ↔ 𝐵 I 𝐴 )