Theorem ideq2

Description: For sets, the identity binary relation is the same as equality. (Contributed by Peter Mazsa, 24-Jun-2020) (Revised by Peter Mazsa, 18-Dec-2021)

	Ref	Expression
Assertion	ideq2	|- ( A e. V -> ( A _I B <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		brid	|- ( A _I B <-> B _I A )
2		ideqg	|- ( A e. V -> ( B _I A <-> B = A ) )
3		eqcom	|- ( B = A <-> A = B )
4	2 3	bitrdi	|- ( A e. V -> ( B _I A <-> A = B ) )
5	1 4	bitrid	|- ( A e. V -> ( A _I B <-> A = B ) )