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\in V\to \left(\left[A\right]{\mathrm{I}}^{-1}=\left[B\right]{\mathrm{I}}^{-1}\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		cnvi	$$⊢{\mathrm{I}}^{-1}=\mathrm{I}$$
2	1	eceq2i	$$⊢\left[A\right]{\mathrm{I}}^{-1}=\left[A\right]\mathrm{I}$$
3		ecidsn	$$⊢\left[A\right]\mathrm{I}=\left\{A\right\}$$
4	2 3	eqtri	$$⊢\left[A\right]{\mathrm{I}}^{-1}=\left\{A\right\}$$
5	1	eceq2i	$$⊢\left[B\right]{\mathrm{I}}^{-1}=\left[B\right]\mathrm{I}$$
6		ecidsn	$$⊢\left[B\right]\mathrm{I}=\left\{B\right\}$$
7	5 6	eqtri	$$⊢\left[B\right]{\mathrm{I}}^{-1}=\left\{B\right\}$$
8	4 7	eqeq12i	$$⊢\left[A\right]{\mathrm{I}}^{-1}=\left[B\right]{\mathrm{I}}^{-1}\leftrightarrow \left\{A\right\}=\left\{B\right\}$$
9		sneqbg	$$⊢A\in V\to \left(\left\{A\right\}=\left\{B\right\}\leftrightarrow A=B\right)$$
10	8 9	syl5bb	$$⊢A\in V\to \left(\left[A\right]{\mathrm{I}}^{-1}=\left[B\right]{\mathrm{I}}^{-1}\leftrightarrow A=B\right)$$