Theorem bj-ideqb

Description: Characterization of classes related by the identity relation. (Contributed by BJ, 24-Dec-2023)

	Ref	Expression
Assertion	bj-ideqb	$$⊢A\mathrm{I}B\leftrightarrow \left(A\in \mathrm{V}\wedge A=B\right)$$

Proof

Step	Hyp	Ref	Expression
1		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
2	1	brrelex1i	$$⊢A\mathrm{I}B\to A\in \mathrm{V}$$
3		inex1g	$$⊢A\in \mathrm{V}\to A\cap B\in \mathrm{V}$$
4		bj-ideqg	$$⊢A\cap B\in \mathrm{V}\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$
5	3 4	syl	$$⊢A\in \mathrm{V}\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$
6	2 5	biadanii	$$⊢A\mathrm{I}B\leftrightarrow \left(A\in \mathrm{V}\wedge A=B\right)$$