Metamath Proof Explorer


Theorem extid

Description: Property of identity relation, see also extep , extssr and the comment of df-ssr . (Contributed by Peter Mazsa, 5-Jul-2019)

Ref Expression
Assertion extid A V A I -1 = B I -1 A = B

Proof

Step Hyp Ref Expression
1 cnvi I -1 = I
2 1 eceq2i A I -1 = A I
3 ecidsn A I = A
4 2 3 eqtri A I -1 = A
5 1 eceq2i B I -1 = B I
6 ecidsn B I = B
7 5 6 eqtri B I -1 = B
8 4 7 eqeq12i A I -1 = B I -1 A = B
9 sneqbg A V A = B A = B
10 8 9 syl5bb A V A I -1 = B I -1 A = B