Metamath Proof Explorer


Theorem ideq2

Description: For sets, the identity binary relation is the same as equality. (Contributed by Peter Mazsa, 24-Jun-2020) (Revised by Peter Mazsa, 18-Dec-2021)

Ref Expression
Assertion ideq2 A V A I B A = B

Proof

Step Hyp Ref Expression
1 brid A I B B I A
2 ideqg A V B I A B = A
3 eqcom B = A A = B
4 2 3 bitrdi A V B I A A = B
5 1 4 syl5bb A V A I B A = B