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	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-br	⊢ ( 𝐴 I 𝐵 ↔ ⟨ 𝐴 , 𝐵 ⟩ ∈ I )
2		bj-opelid	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( ⟨ 𝐴 , 𝐵 ⟩ ∈ I ↔ 𝐴 = 𝐵 ) )
3	1 2	bitrid	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ 𝑉 → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )