This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem brid

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

Ref Expression
Assertion brid ⊢ A I B ↔ B I A

Proof

Step Hyp Ref Expression
1 cnvi ⊢ I -1 = I
2 1 breqi ⊢ A I -1 B ↔ A I B
3 reli ⊢ Rel ⁡ I
4 3 relbrcnv ⊢ A I -1 B ↔ B I A
5 2 4 bitr3i ⊢ A I B ↔ B I A