Theorem ideq2

Description: For sets, the identity binary relation is the same as equality. (Contributed by Peter Mazsa, 24-Jun-2020) (Revised by Peter Mazsa, 18-Dec-2021)

	Ref	Expression
Assertion	ideq2	$$⊢A\in V\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		brid	$$⊢A\mathrm{I}B\leftrightarrow B\mathrm{I}A$$
2		ideqg	$$⊢A\in V\to \left(B\mathrm{I}A\leftrightarrow B=A\right)$$
3		eqcom	$$⊢B=A\leftrightarrow A=B$$
4	2 3	bitrdi	$$⊢A\in V\to \left(B\mathrm{I}A\leftrightarrow A=B\right)$$
5	1 4	bitrid	$$⊢A\in V\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$