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 ( 𝐴 ∈ 𝑉 → ( [ 𝐴 ] ◡ I = [ 𝐵 ] ◡ I ↔ 𝐴 = 𝐵 ) )

Proof

Step Hyp Ref Expression
1 cnvi ⊢ ◡ I = I
2 1 eceq2i ⊢ [ 𝐴 ] ◡ I = [ 𝐴 ] I
3 ecidsn ⊢ [ 𝐴 ] I = { 𝐴 }
4 2 3 eqtri ⊢ [ 𝐴 ] ◡ I = { 𝐴 }
5 1 eceq2i ⊢ [ 𝐵 ] ◡ I = [ 𝐵 ] I
6 ecidsn ⊢ [ 𝐵 ] I = { 𝐵 }
7 5 6 eqtri ⊢ [ 𝐵 ] ◡ I = { 𝐵 }
8 4 7 eqeq12i ⊢ ( [ 𝐴 ] ◡ I = [ 𝐵 ] ◡ I ↔ { 𝐴 } = { 𝐵 } )
9 sneqbg ⊢ ( 𝐴 ∈ 𝑉 → ( { 𝐴 } = { 𝐵 } ↔ 𝐴 = 𝐵 ) )
10 8 9 bitrid ⊢ ( 𝐴 ∈ 𝑉 → ( [ 𝐴 ] ◡ I = [ 𝐵 ] ◡ I ↔ 𝐴 = 𝐵 ) )