Theorem ideq

Description: For sets, the identity relation is the same as equality. (Contributed by NM, 13-Aug-1995)

	Ref	Expression
Hypothesis	ideq.1	⊢ 𝐵 ∈ V
Assertion	ideq	⊢ ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		ideq.1	⊢ 𝐵 ∈ V
2		ideqg	⊢ ( 𝐵 ∈ V → ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 ) )
3	1 2	ax-mp	⊢ ( 𝐴 I 𝐵 ↔ 𝐴 = 𝐵 )