Theorem brid

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

	Ref	Expression
Assertion	brid	$$⊢A\mathrm{I}B\leftrightarrow B\mathrm{I}A$$

Proof

Step	Hyp	Ref	Expression
1		cnvi	$$⊢{\mathrm{I}}^{-1}=\mathrm{I}$$
2	1	breqi	$$⊢A{\mathrm{I}}^{-1}B\leftrightarrow A\mathrm{I}B$$
3		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
4	3	relbrcnv	$$⊢A{\mathrm{I}}^{-1}B\leftrightarrow B\mathrm{I}A$$
5	2 4	bitr3i	$$⊢A\mathrm{I}B\leftrightarrow B\mathrm{I}A$$