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 ↔ 𝐴 = 𝐵 ) )