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 = _I
2 1 breqi 
 |-  ( A `' _I B <-> A _I B )
3 reli 
 |-  Rel _I
4 3 relbrcnv 
 |-  ( A `' _I B <-> B _I A )
5 2 4 bitr3i 
 |-  ( A _I B <-> B _I A )