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

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 bitrid ⊢ A ∈ V → A I -1 = B I -1 ↔ A = B