Theorem ideq

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

	Ref	Expression
Hypothesis	ideq.1	|- B e. _V
Assertion	ideq	|- ( A _I B <-> A = B )

Proof

Step	Hyp	Ref	Expression
1		ideq.1	|- B e. _V
2		ideqg	|- ( B e. _V -> ( A _I B <-> A = B ) )
3	1 2	ax-mp	|- ( A _I B <-> A = B )