Theorem bj-ideqg

Description: Characterization of the classes related by the identity relation when their intersection is a set. Note that the antecedent is more general than either class being a set. (Contributed by NM, 30-Apr-2004) Weaken the antecedent to sethood of the intersection. (Revised by BJ, 24-Dec-2023)

TODO: replace ideqg , or at least prove ideqg from it.

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

Proof

Step	Hyp	Ref	Expression
1		df-br	$$⊢A\mathrm{I}B\leftrightarrow ⟨A,B⟩\in \mathrm{I}$$
2		bj-opelid	$$⊢A\cap B\in V\to \left(⟨A,B⟩\in \mathrm{I}\leftrightarrow A=B\right)$$
3	1 2	bitrid	$$⊢A\cap B\in V\to \left(A\mathrm{I}B\leftrightarrow A=B\right)$$