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 i^i B ) e. V -> ( A _I B <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	|- ( A _I B <-> <. A , B >. e. _I )
2		bj-opelid	|- ( ( A i^i B ) e. V -> ( <. A , B >. e. _I <-> A = B ) )
3	1 2	syl5bb	|- ( ( A i^i B ) e. V -> ( A _I B <-> A = B ) )