Theorem bj-ideqb

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

	Ref	Expression
Assertion	bj-ideqb	⊢ ( 𝐴 I 𝐵 ↔ ( 𝐴 ∈ V ∧ 𝐴 = 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		reli	⊢ Rel I
2	1	brrelex1i	⊢ ( 𝐴 I 𝐵 → 𝐴 ∈ V )
3		inex1g	⊢ ( 𝐴 ∈ V → ( 𝐴 ∩ 𝐵 ) ∈ V )
4		bj-ideqg	⊢ ( ( 𝐴 ∩ 𝐵 ) ∈ V → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )
5	3 4	syl	⊢ ( 𝐴 ∈ V → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )
6	2 5	biadanii	⊢ ( 𝐴 I 𝐵 ↔ ( 𝐴 ∈ V ∧ 𝐴 = 𝐵 ) )